proposition: Lemma trmx_lrsub : (lrsubmx A)^T === lrsubmx A^T.
proof: Proof. by move => i j /=; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms