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