proposition: Lemma eqmod_contraction b a: natp a -> natp b -> b <> \0c -> a = the_contraction (csucc b) a %c[mod b].
proof: Proof. move => aN bN bnz. have sbN := NS_succ bN; have cb := (CS_nat bN). have bg1: \1c <c (csucc b). apply /(cltSleP bN); exact:(cge1 (CS_nat bN) bnz). move:(the_expansion_pr sbN bg1 aN). rewrite/the_contraction; set f := the_expansion _ _. move => [[ha hb] hc]; rewrite - hb. apply:(eqmod_pow3 bN bnz ha). rewrite (csucc_pr4 cb) - {1} (cprod1r cb); apply:crem_prop; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)