proposition: Lemma cprodBl a b c: natp a -> natp b -> natp c -> a *c (b -c c) = (a *c b) -c (a *c c).
proof: Proof. move=> aN bN cN. case: (NleT_ee bN cN) => le. by rewrite (cdiff_wrong le) (cdiff_wrong (cprod_Meqle a le)) (cprod0r). symmetry; apply: cdiff_pr2; fprops; rewrite - cprodDr csumC cdiff_pr //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)