proposition: Lemma cprodACA: interchange cprod2 cprod2.
proof: Proof. move => s1 s2 r1 r2; rewrite (cprodA _ s2 r2) (cprodA _ r1 r2). by rewrite -(cprodA s1) (cprodC s2 r1) (cprodA s1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)