proposition: Lemma cprod_via_sum a b: cardinalp b -> a *c (csucc b) = (a *c b) +c a.
proof: Proof. move=> cb; rewrite (csucc_pr4 cb) cprodDr. rewrite - (csum2cr (a *c b) a) - (cprod1l (CS_cardinal a)). by rewrite (cprod2cr \1c a) (cprodC \1c). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)