proposition: Lemma mulcm_eq0 m1 m2 : mulcm m1 m2 = onecm -> m1 = onecm /\ m2 = onecm.
proof: Proof. move: m1 m2; have gen m1 m2 : mulcm m1 m2 = onecm -> m1 = onecm. move/eqP/cmP=> h; apply/eqP/cmP=> i; move/eqP: (h i). by rewrite mulcmE onecmE addn_eq0 => /andP[] /eqP->. by move=> m1 m2 h; split; move: h; last rewrite mulcmC; apply/gen. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap