proposition: Lemma trmx_mul : forall m n p (A : matrix R m n) (B : 'M_(n, p)), (A *m B)^T === B^T *m A^T.
proof: Proof. move=> m n p A B; rewrite -> trmx_mul_rev; rewrite /mulmx=> k i. by apply (eq_bigr (I:=ordinal_finType n)) => j _; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms