@@ -697,6 +697,22 @@ maximumSuccSucc (S left) (S right) =
697697 let inductiveHypothesis = maximumSuccSucc left right in
698698 ?maximumSuccSuccStepCase
699699
700+total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
701+sucMaxL Z = refl
702+sucMaxL (S l) = cong (sucMaxL l)
703+
704+total sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
705+sucMaxR Z = refl
706+sucMaxR (S l) = cong (sucMaxR l)
707+
708+total sucMinL : (l : Nat) -> minimum (S l) l = l
709+sucMinL Z = refl
710+sucMinL (S l) = cong (sucMinL l)
711+
712+total sucMinR : (l : Nat) -> minimum l (S l) = l
713+sucMinR Z = refl
714+sucMinR (S l) = cong (sucMinR l)
715+
700716-- div and mod
701717total modZeroZero : (n : Nat) -> mod 0 n = Z
702718modZeroZero Z = refl