proposition: Lemma carryandplus ( a b : fpscommring hz ) : carry ( a + b ) = carry ( carry a + carry b ).
proof: Proof. intros. assert ( forall n : nat, carry ( a + b ) n = ( carry ( carry a + carry b ) n ) ) as f. { intros n. destruct n. - change ( hzremaindermod m is ( a 0%nat + b 0%nat ) = hzremaindermod m is ( hzremaindermod m is ( a 0%nat ) + hzremaindermod m is ( b 0%nat ) ) ). rewrite hzremaindermodandplus. apply idpath. - change ( hzremaindermod m is ( a ( S n ) + b ( S n ) + hzquotientmod m is ( precarry ( a + b ) n ) ) = hzremaindermod m is ( hzremaindermod m is ( a ( S n ) + hzquotientmod m is ( precarry a n ) ) + hzremaindermod m is ( b ( S n ) + hzquotientmod m is ( precarry b n ) ) + hzquotientmod m is ( precarry ( carry a + carry b ) n ) ) ). rewrite quotientprecarryplus. rewrite ( hzremaindermodandplus m is ( hzremaindermod m is (a (S n) + hzquotientmod m is (precarry a n)) + hzremaindermod m is (b (S n) + hzquotientmod m is (precarry b n)) ) _ ). change (hzremaindermod m is (a (S n) + hzquotientmod m is (precarry a n)) + hzremaindermod m is (b (S n) + hzquotientmod m is (precarry b n))) with (hzremaindermod m is (a (S n) + hzquotientmod m is (precarry a n))%ring + hzremaindermod m is (b (S n) + hzquotientmod m is (precarry b n))%ring)%hz. + rewrite <- (hzremaindermodandplus m is (a (S n) + hzquotientmod m is (precarry a n)) (b (S n) + hzquotientmod m is (precarry b n)) ). rewrite <- hzremaindermodandplus. change ( ((a (S n) + hzquotientmod m is (precarry a n))%ring + (b (S n) + hzquotientmod m is (precarry b n))%ring + hzquotientmod m is (precarry (carry a + carry b)%ring n))%hz ) with ((a (S n) + hzquotientmod m is (precarry a n))%ring + (b (S n) + hzquotientmod m is (precarry b n))%ring + hzquotientmod m is (precarry (carry a + carry b)%ring n))%ring. rewrite <- ( ringassoc1 hz ( a ( S n ) + hzquotientmod m is ( precarry a n ) ) (b (S n) ) ( hzquotientmod m is (precarry b n)) ). rewrite ( ringassoc1 hz ( a ( S n ) ) (hzquotientmod m is ( precarry a n ) ) ( b ( S n ) ) ). rewrite ( ringcomm1 hz ( hzquotientmod m is ( precarry a n ) ) ( b ( S n ) ) ). rewrite <- 3! ( ringassoc1 hz ). apply idpath. } apply ( funextfun _ _ f ). Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers