Lemma quotientprecarryplus ( a b : fpscommring hz ) ( n : nat ) : hzquotientmod m is ( precarry ( a + b ) n ) = hzquotientmod m is ( precarry a n ) + hzquotientmod m is ( precarry b n ) + hzquotientmod m is ( precarry ( carry a + carry b ) n ). Proof. intros. induction n. - simpl. change ( hzquotientmod m is ( a 0%nat + b 0%nat ) = hzquotientmod m is (a 0%nat) + hzquotientmod m is (b 0%nat) + hzquotientmod m is ( hzremaindermod m is ( a 0%nat ) + hzremaindermod m is ( b 0%nat ) ) ). rewrite hzquotientmodandplus. apply idpath. - change ( hzquotientmod m is ( a ( S n ) + b ( S n ) + hzquotientmod m is ( precarry (a + b) n ) ) = hzquotientmod m is (precarry a (S n)) + hzquotientmod m is (precarry b (S n)) + hzquotientmod m is (carry a ( S n ) + carry b ( S n ) + hzquotientmod m is ( precarry (carry a + carry b) n)) ). rewrite IHn. rewrite ( ringassoc1 hz ( a ( S n ) ) ( b ( S n ) ) _ ). rewrite <- ( ringassoc1 hz ( b ( S n ) ) ). rewrite ( ringcomm1 hz ( b ( S n ) ) _ ). rewrite <- 3! ( ringassoc1 hz ( a ( S n ) ) _ _ ). change ( a ( S n ) + hzquotientmod m is ( precarry a n ) ) with ( precarry a ( S n ) ). set ( pa := precarry a ( S n ) ). rewrite ( ringassoc1 hz pa _ ( b ( S n ) ) ). rewrite ( ringcomm1 hz _ ( b ( S n ) ) ). change ( b ( S n ) + hzquotientmod m is ( precarry b n ) ) with ( precarry b ( S n ) ). set ( pb := precarry b ( S n ) ). set ( ab := precarry ( carry a + carry b ) ). rewrite ( ringassoc1 hz ( carry a ( S n ) ) ( carry b ( S n ) ) ( hzquotientmod m is ( ab n ) ) ). rewrite ( hzquotientmodandplus m is ( carry a ( S n ) ) _ ). unfold carry at 1. rewrite <- hzqrandremainderq. rewrite hzplusl0. rewrite ( hzquotientmodandplus m is ( carry b ( S n ) ) _ ). unfold carry at 1. rewrite <- hzqrandremainderq. rewrite hzplusl0. rewrite ( ringassoc1 hz pa pb _ ). rewrite ( hzquotientmodandplus m is pa _ ). change (pb + hzquotientmod m is (ab n)) with (pb + hzquotientmod m is (ab n))%hz. rewrite ( hzquotientmodandplus m is pb ( hzquotientmod m is ( ab n ) ) ). rewrite <- 2! ( ringassoc1 hz ( hzquotientmod m is pa ) _ _ ). rewrite <- 2! ( ringassoc1 hz ( hzquotientmod m is pa + hzquotientmod m is pb ) _ ). rewrite 2! ( ringassoc1 hz ( hzquotientmod m is pa + hzquotientmod m is pb + hzquotientmod m is (hzquotientmod m is (ab n)) ) _ _ ). apply ( maponpaths ( fun x : hz => hzquotientmod m is pa + hzquotientmod m is pb + hzquotientmod m is (hzquotientmod m is (ab n)) + x ) ). unfold carry at 1 2. rewrite 2! hzremaindermoditerated. change ( precarry b ( S n ) ) with pb. change ( precarry a ( S n ) ) with pa. apply ( maponpaths ( fun x : hz => ( hzquotientmod m is (hzremaindermod m is pb + hzremaindermod m is (hzquotientmod m is (ab n)))%hz ) + x ) ). apply maponpaths. apply ( maponpaths ( fun x : hz => hzremaindermod m is pa + x ) ). rewrite ( hzremaindermodandplus m is ( carry b ( S n ) ) _ ). unfold carry. rewrite hzremaindermoditerated. rewrite <- ( hzremaindermodandplus m is ( precarry b ( S n ) ) _ ). apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.PAdics.fps. Require Import UniMath.PAdics.frac. Require Import UniMath.PAdics.z_mod_p. Require Import UniMath.NumberSystems.Integers.