proposition: Lemma ntensmx1 : forall {m n} (A : 'M_(m,n)) , A ^t 1 = A.
proof: Proof. by []. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)