@@ -631,8 +631,40 @@ lteSuccZeroFalse Z = refl
631631lteSuccZeroFalse (S n) = refl
632632
633633-- Minimum and maximum
634+total maximumAssociative : (l,c,r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r
635+maximumAssociative Z c r = refl
636+maximumAssociative (S k) Z r = refl
637+maximumAssociative (S k) (S j) Z = refl
638+maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in refl
639+
640+total maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l
641+maximumCommutative Z Z = refl
642+maximumCommutative Z (S k) = refl
643+maximumCommutative (S k) Z = refl
644+maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in refl
645+
646+total maximumIdempotent : (n : Nat) -> maximum n n = n
647+maximumIdempotent Z = refl
648+maximumIdempotent (S k) = cong (maximumIdempotent k)
649+
650+total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r
651+minimumAssociative Z c r = refl
652+minimumAssociative (S k) Z r = refl
653+minimumAssociative (S k) (S j) Z = refl
654+minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in refl
655+
656+total minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l
657+minimumCommutative Z Z = refl
658+minimumCommutative Z (S k) = refl
659+minimumCommutative (S k) Z = refl
660+minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in refl
661+
662+total minimumIdempotent : (n : Nat) -> minimum n n = n
663+minimumIdempotent Z = refl
664+minimumIdempotent (S k) = cong (minimumIdempotent k)
665+
634666total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
635−minimumZeroZeroRight Z = refl
667+minimumZeroZeroRight Z = refl
636668minimumZeroZeroRight (S right) = minimumZeroZeroRight right
637669
638670total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
@@ -648,15 +680,6 @@ minimumSuccSucc (S left) (S right) =
648680 let inductiveHypothesis = minimumSuccSucc left right in
649681 ?minimumSuccSuccStepCase
650682
651−total minimumCommutative : (left : Nat) -> (right : Nat) ->
652− minimum left right = minimum right left
653−minimumCommutative Z Z = refl
654−minimumCommutative Z (S right) = refl
655−minimumCommutative (S left) Z = refl
656−minimumCommutative (S left) (S right) =
657− let inductiveHypothesis = minimumCommutative left right in
658− ?minimumCommutativeStepCase
659−
660683total maximumZeroNRight : (right : Nat) -> maximum Z right = right
661684maximumZeroNRight Z = refl
662685maximumZeroNRight (S right) = refl
@@ -674,15 +697,6 @@ maximumSuccSucc (S left) (S right) =
674697 let inductiveHypothesis = maximumSuccSucc left right in
675698 ?maximumSuccSuccStepCase
676699
677−total maximumCommutative : (left : Nat) -> (right : Nat) ->
678− maximum left right = maximum right left
679−maximumCommutative Z Z = refl
680−maximumCommutative (S left) Z = refl
681−maximumCommutative Z (S right) = refl
682−maximumCommutative (S left) (S right) =
683− let inductiveHypothesis = maximumCommutative left right in
684− ?maximumCommutativeStepCase
685−
686700-- div and mod
687701total modZeroZero : (n : Nat) -> mod 0 n = Z
688702modZeroZero Z = refl
@@ -848,28 +862,12 @@ plusZeroRightNeutralStepCase = proof {
848862 trivial;
849863}
850864
851−maximumCommutativeStepCase = proof {
852− intros;
853− rewrite (boolElimSuccSucc (lte left right) right left);
854− rewrite (boolElimSuccSucc (lte right left) left right);
855− rewrite inductiveHypothesis;
856− trivial;
857−}
858−
859865maximumSuccSuccStepCase = proof {
860866 intros;
861867 rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));
862868 trivial;
863869}
864870
865−minimumCommutativeStepCase = proof {
866− intros;
867− rewrite (boolElimSuccSucc (lte left right) left right);
868− rewrite (boolElimSuccSucc (lte right left) right left);
869− rewrite inductiveHypothesis;
870− trivial;
871−}
872−
873871minimumSuccSuccStepCase = proof {
874872 intros;
875873 rewrite (boolElimSuccSucc (lte left right) (S left) (S right));