proposition: Lemma BZrem_cN a b: natp a -> natp b -> (BZ_of_nat a) %%z (BZ_of_nat b) = BZ_of_nat (a%%c b).
proof: Proof. move => aN bN. move: (BZ_of_nat_i aN) => az. move: (BZ_of_nat_i bN) => bz. case: (equal_or_not b \0c) => bc. by rewrite bc (crem_zero aN) (proj1 (BZ_quorem0 az)). have bbnz: (BZ_of_nat b) <> \0z by move/pr1_def. move:(BZdvd_correct az bz bbnz) => [ _ _ [h _ _]]. move: (cdivision aN bN bc) => [sa sb [sc sd]]. move: (BZ_of_nat_i (NS_prod bN sa))(BZ_of_nat_i sb) => ha hb. move: h; rewrite (BZquo_cN aN bN) {1} sc - (BZsum_cN (NS_prod bN sa) sb). by rewrite (BZprod_cN bN sa); move/(BZsum_eq2l ha hb (ZS_rem az bz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)