proposition: Lemma tr_copid_mx m r : (copid_mx r)^T = @copid_mx R m r.
proof: Proof. apply/matrixP=> i j; rewrite !mxE eq_sym. case: eqP=> [->|/eqP hij] //=; rewrite eq_sym. by have -> : (i == j :> nat) = false by apply/eqP/eqP. 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