proposition: Lemma tensmx_unit (R : fieldType) m n (A : 'M[R]_m%N) (B : 'M[R]_n%N) : m != 0%N -> n != 0%N -> A \in unitmx -> B \in unitmx -> (A *t B) \in unitmx.
proof: Proof. move: m n A B => [|m] [|n] // A B _ _ uA uB. suff : (A^-1 *t B^-1) *m (A *t B) = 1 by case/mulmx1_unit. rewrite tensmx_mul !mulVmx //; apply/matrixP=> /= i j. rewrite !mxE /=; symmetry; rewrite -natrM -!val_eqE /=. rewrite {1}(divn_eq i n.+1) {1}(divn_eq j n.+1). by rewrite eq_addl_mul ?ltn_mod // xpair_eqE mulnb. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)