fact: Definition pid_seqmx m n r := mkseqmx_ord (fun (i : 'I_m) (j : 'I_n) => if (eqn i j) && (i < r) then 1%C else 0%C).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly matrix mxpoly) CoqEAL(hrel param refinements trivial_seq)