proposition: Lemma lower_triangular_mxP m n (M : 'M[R]_(m,n)) : lower_triangular_mx M <-> upper_triangular_mx M^T.
proof: Proof. rewrite /lower_triangular_mx /upper_triangular_mx. rewrite /lower_part_mx /upper_part_mx. split=> [/eqP ->|/eqP H]; apply/eqP. by apply/matrixP=> i j; rewrite !mxE; case: leqP. by rewrite -[M]trmxK H; apply/matrixP=> i j; rewrite !mxE; case: leqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm poly mxpoly finfun tuple) mathcomp(matrix bigop zmodp polydiv) ssrcomplements dvdring