@@ -512,19 +512,18 @@ plusLeftCancel (S left) right right' p =
512512
513513total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
514514 (p : left + right = left' + right) -> left = left'
515−plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in
516− rewrite sym (plusZeroRightNeutral left') in
517− p
518−plusRightCancel left left' (S right) p =
519− plusRightCancel left left' right
520− (succInjective _ _ (rewrite plusSuccRightSucc left right in
521− rewrite plusSuccRightSucc left' right in p))
515+plusRightCancel left left' right p =
516+ plusLeftCancel right left left' $
517+ rewrite plusCommutative right left in
518+ rewrite plusCommutative right left' in
519+ p
522520
523521total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
524522 (p : left + right = left) -> right = Z
525−plusLeftLeftRightZero Z right p = p
526−plusLeftLeftRightZero (S left) right p =
527− plusLeftLeftRightZero left right (succInjective _ _ p)
523+plusLeftLeftRightZero left right p =
524+ plusLeftCancel left right Z $
525+ rewrite plusZeroRightNeutral left in
526+ p
528527
529528-- Mult
530529total multZeroLeftZero : (right : Nat) -> Z * right = Z
@@ -573,12 +572,11 @@ multDistributesOverPlusRight (S left) centre right =
573572
574573total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
575574 (left + centre) * right = (left * right) + (centre * right)
576−multDistributesOverPlusLeft Z centre right = Refl
577−multDistributesOverPlusLeft (S left) centre right =
578− let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
579− rewrite inductiveHypothesis in
580− rewrite plusAssociative right (mult left right) (mult centre right) in
581− Refl
575+multDistributesOverPlusLeft left centre right =
576+ rewrite multCommutative (left + centre) right in
577+ rewrite multCommutative left right in
578+ rewrite multCommutative centre right in
579+ multDistributesOverPlusRight right left centre
582580
583581total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
584582 left * (centre * right) = (left * centre) * right
@@ -597,11 +595,7 @@ multOneLeftNeutral (S right) =
597595 Refl
598596
599597total multOneRightNeutral : (left : Nat) -> left * 1 = left
600−multOneRightNeutral Z = Refl
601−multOneRightNeutral (S left) =
602− let inductiveHypothesis = multOneRightNeutral left in
603− rewrite inductiveHypothesis in
604− Refl
598+multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left
605599
606600-- Minus
607601total minusSuccSucc : (left : Nat) -> (right : Nat) ->
@@ -689,10 +683,7 @@ total powerZeroOne : (base : Nat) -> power base 0 = S Z
689683powerZeroOne base = Refl
690684
691685total powerOneNeutral : (base : Nat) -> power base 1 = base
692−powerOneNeutral Z = Refl
693−powerOneNeutral (S base) =
694− let inductiveHypothesis = powerOneNeutral base in
695− rewrite inductiveHypothesis in Refl
686+powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
696687
697688total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
698689powerOneSuccOne Z = Refl
@@ -701,8 +692,7 @@ powerOneSuccOne (S exp) =
701692 rewrite inductiveHypothesis in Refl
702693
703694total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
704−powerSuccSuccMult Z = Refl
705−powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl
695+powerSuccSuccMult base = rewrite multOneRightNeutral base in Refl
706696
707697total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
708698 power (power base exp) exp' = power base (exp * exp')
@@ -796,34 +786,24 @@ minimumIdempotent Z = Refl
796786minimumIdempotent (S k) = cong (minimumIdempotent k)
797787
798788total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
799−minimumZeroZeroRight Z = Refl
800−minimumZeroZeroRight (S right) = minimumZeroZeroRight right
789+minimumZeroZeroRight right = Refl
801790
802791total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
803−minimumZeroZeroLeft Z = Refl
804−minimumZeroZeroLeft (S left) = Refl
792+minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl
805793
806794total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
807795 minimum (S left) (S right) = S (minimum left right)
808−minimumSuccSucc Z Z = Refl
809−minimumSuccSucc (S left) Z = Refl
810−minimumSuccSucc Z (S right) = Refl
811−minimumSuccSucc (S left) (S right) = Refl
796+minimumSuccSucc left right = Refl
812797
813798total maximumZeroNRight : (right : Nat) -> maximum Z right = right
814−maximumZeroNRight Z = Refl
815−maximumZeroNRight (S right) = Refl
799+maximumZeroNRight right = Refl
816800
817801total maximumZeroNLeft : (left : Nat) -> maximum left Z = left
818−maximumZeroNLeft Z = Refl
819−maximumZeroNLeft (S left) = Refl
802+maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl
820803
821804total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
822805 S (maximum left right) = maximum (S left) (S right)
823−maximumSuccSucc Z Z = Refl
824−maximumSuccSucc (S left) Z = Refl
825−maximumSuccSucc Z (S right) = Refl
826−maximumSuccSucc (S left) (S right) = Refl
806+maximumSuccSucc left right = Refl
827807
828808total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
829809sucMaxL Z = Refl