@@ -557,26 +557,21 @@ multCommutative (S left) right =
557557 rewrite multRightSuccPlus right left in
558558 Refl
559559
560−total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
561− left * (centre + right) = (left * centre) + (left * right)
562−multDistributesOverPlusRight Z centre right = Refl
563−multDistributesOverPlusRight (S left) centre right =
564− let inductiveHypothesis = multDistributesOverPlusRight left centre right in
565− rewrite inductiveHypothesis in
566− rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in
567− rewrite sym (plusAssociative centre (mult left centre) right) in
568− rewrite plusCommutative (mult left centre) right in
569− rewrite plusAssociative centre right (mult left centre) in
570− rewrite plusAssociative (plus centre right) (mult left centre) (mult left right) in
571− Refl
572−
573560total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
574561 (left + centre) * right = (left * right) + (centre * right)
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
562+multDistributesOverPlusLeft Z centre right = Refl
563+multDistributesOverPlusLeft (S k) centre right =
564+ rewrite multDistributesOverPlusLeft k centre right in
565+ rewrite plusAssociative right (k * right) (centre * right) in
566+ Refl
567+
568+total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
569+ left * (centre + right) = (left * centre) + (left * right)
570+multDistributesOverPlusRight left centre right =
571+ rewrite multCommutative left (centre + right) in
572+ rewrite multCommutative left centre in
573+ rewrite multCommutative left right in
574+ multDistributesOverPlusLeft centre right left
580575
581576total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
582577 left * (centre * right) = (left * centre) * right
@@ -588,11 +583,7 @@ multAssociative (S left) centre right =
588583 Refl
589584
590585total multOneLeftNeutral : (right : Nat) -> 1 * right = right
591−multOneLeftNeutral Z = Refl
592−multOneLeftNeutral (S right) =
593− let inductiveHypothesis = multOneLeftNeutral right in
594− rewrite inductiveHypothesis in
595− Refl
586+multOneLeftNeutral right = plusZeroRightNeutral right
596587
597588total multOneRightNeutral : (left : Nat) -> left * 1 = left
598589multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left