proposition: Lemma cdivision_prop_alt a b q r: natp a -> natp b -> natp q -> natp r -> b <> \0c -> (cdivision_prop a b q r <-> [/\ (b *c q) <=c a, a <c (b *c csucc q) & r = a -c (b *c q)]).
proof: Proof. move=> aN bN qN rN nzb; rewrite /cdivision_prop. set (w:= b *c q). rewrite Nsucc_rw // cprodC cprodDl cprodC cprod1l; fprops. have wN: natp w by rewrite /w; fprops. split. move=> [av lt];split => //. - by rewrite av; apply: Nsum_M0le. - rewrite av; apply: csum_Mlelt; fprops. - by symmetry;apply: cdiff_pr2 =>//; symmetry; rewrite csumC. move=> [lwa ltas rv]. rewrite rv. have aux: natp (b *c q +c b) by fprops. split; first by symmetry; apply: cdiff_pr =>//. move: ltas => /(card_ltP aN aux) [c [cN nzc s]] {aux}. move: (cdiff_pr lwa); rewrite -rv=> aux. apply /(card_ltP rN bN); exists c => //; split => //. by apply: (csum_eq2l wN (NS_sum rN cN) bN);rewrite csumA aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)