proposition: Lemma m3lmulP l1 l2: GRing.comm (m3lmx l1) (m3lmx l2) -> m3lmx (m3lmul l1 l2) = m3lmx l1 * m3lmx l2.
proof: Proof. move=> hcomm. apply/matrixP=> [][ [ | [| i]] ip] [ [ | [| j]] jp] //=; rewrite /m3lmx /m3lmul !mxE; set a1 := nth Z0 l1 0; set b1 := nth Z0 l1 2; set d1 := nth Z0 l1 1; set a2 := nth Z0 l2 0; set b2 := nth Z0 l2 2; set d2 := nth Z0 l2 1; rewrite /=; rewrite !big_ord_recr /= big_ord0 /= add0r /=; rewrite !mxE; cbn -[nth]; rewrite -/a1 -/a2 -/b1 -/b2 -/d1 -/d2 /=; rewrite ?(ZtoRD, ZtoRM). apply erefl. apply erefl. move: hcomm => /matrixP/(_ ord0 (inord 1)). rewrite !mxE 2!big_ord_recr big_ord0 /= add0r. rewrite /m3lmx !mxE -/a1 -/a2 -/b1 -/b2 -/d1 -/d2 /=. rewrite -!(inj_eq val_inj) /= inordK //=. rewrite 2!big_ord_recr big_ord0 /= add0r. rewrite /m3lmx !mxE -/a1 -/a2 -/b1 -/b2 -/d1 -/d2 /=. rewrite -!(inj_eq val_inj) /= inordK //= => ->. by congr (_ + _); rewrite mulrC. apply erefl. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)