proposition: Lemma eqmod_contraction_rep b a (x := contraction_rep (csucc b) a) (y := a %%c b) : natp a -> natp b -> b <> \0c -> [/\ a = x %c[mod b], (a = \0c -> x = \0c) & (a <> \0c -> (y = \0c -> x = b) /\ (y <> \0c -> x = y))].
proof: Proof. move => aN bN bnz. have sbN := NS_succ bN. have bg1: \1c <c (csucc b). apply /(cltSleP bN); exact:(cge1 (CS_nat bN) bnz). have hrec: forall n, natp n -> a = (Vf (contraction_rec (csucc b) a) n) %c[mod b]. apply:Nat_induction; first by rewrite contraction_rec0. move => n nN; rewrite (contraction_rec_succ _ _ nN) => {1} ->. by apply:eqmod_contraction=> //;apply: NS_contraction_rec. have h: a = x %c[mod b] by apply:hrec. move:(contraction_rep_dig sbN bg1 aN); rewrite -/x. move /(cltSleP bN) => lexb. have xN := NS_le_nat lexb bN. split => // ha. by rewrite /x ha /contraction_rep contraction_rec0. move:(contraction_rep_non_zero sbN bg1 aN ha); rewrite -/x /y h => xnz. case (equal_or_not x b) => xeb. by split => //; rewrite xeb (proj33(cdivides_itself bN)). by rewrite-(crem_small bN (conj lexb xeb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)