proposition: Lemma cprodA a b c: a *c (b *c c) = (a *c b) *c c.
proof: Proof. rewrite (cprodC (a *c b)) !cprod2_pr1 !cprod2_pr2. move /card_eqP: (Eq_mulA a b c) => ->. by rewrite -!cprod2_pr1 cprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)