ordering

Ordering.flipFlip

def flipFlip (o : Ordering) : flip (flip o) = o

Flipping twice gives the result back.

Ordering.isLTFlip

def isLTFlip (o : Ordering) : isLT o = isGT (flip o)

LT exactly when the flip is GT.

Ordering.isGTFlip

def isGTFlip (o : Ordering) : isGT o = isLT (flip o)

GT exactly when the flip is LT.

Ordering.isEQFlip

def isEQFlip (o : Ordering) : isEQ o = isEQ (flip o)

EQ exactly when the flip is EQ.

Ordering.beqRefl

def beqRefl (o : Ordering) : beq o o = true

A result is the same as itself.

Ordering.beqSymmetric

def beqSymmetric (a : Ordering) (b : Ordering) : beq a b = beq b a

Whether two results are the same does not depend on the order they are asked in.

Ordering.thenAssociative

def thenAssociative (a : Ordering) (b : Ordering) (c : Ordering) : r#then (r#then a b) c = r#then a (r#then b c)

then is associative.

Ordering.eqThen

def eqThen (o : Ordering) : r#then EQ o = o

EQ then anything is that thing.

Ordering.thenEq

def thenEq (o : Ordering) : r#then o EQ = o

Anything then EQ is that thing.

Ordering.flipThen

def flipThen (a : Ordering) (b : Ordering) : flip (r#then a b) = r#then (flip a) (flip b)

Flipping a combination is combining the flips.

Nat.threeWayStructurallyRefl

def Nat.threeWayStructurallyRefl (n : Nat) : Nat.threeWayStructurally n n = EQ

Every natural compares equal to itself (structurally).

Nat.threeWayStructurallyFlip

def Nat.threeWayStructurallyFlip (m : Nat) (n : Nat) : Nat.threeWayStructurally m n = Ordering.flip (Nat.threeWayStructurally n m)

Comparing the other way round is the flip (structurally).

Nat.threeWayStructurallyIsLT

def Nat.threeWayStructurallyIsLT (m : Nat) (n : Nat) : Ordering.isLT (Nat.threeWayStructurally m n) = Nat.blt m n

The structural comparison is LT exactly when Nat.blt is true.

Nat.threeWayStructurallyIsEQ

def Nat.threeWayStructurallyIsEQ (m : Nat) (n : Nat) : Ordering.isEQ (Nat.threeWayStructurally m n) = Nat.beq m n

The structural comparison is EQ exactly when Nat.beq is true.

Nat.threeWayRefl

def Nat.threeWayRefl (n : Nat) : Nat.threeWay n n = EQ

Every natural compares equal to itself.

Bool.threeWayRefl

def Bool.threeWayRefl (b : Bool) : Bool.threeWay b b = EQ

Every Boolean compares equal to itself.

Bool.threeWayFlip

def Bool.threeWayFlip (a : Bool) (b : Bool) : Bool.threeWay a b = Ordering.flip (Bool.threeWay b a)

Comparing Booleans the other way round is the flip.