proposition: Lemma Rseqmx_spec_seqmx m n (M : @seqmx A) : (size M == m) && all (fun r => size r == n) M -> Rseqmx (nat_Rxx m) (nat_Rxx n) (spec_seqmx m n M) M.
proof: Proof. move/andP=>[] /eqP Hm /all_nthP Hn; split=>[//||]. { by move=> i Hi; apply/eqP /Hn; rewrite Hm. } move=> i j; rewrite mxE. rewrite /map_seqmx /spec /spec_of_instance_0 /spec_id /=. by rewrite (nth_map [::]) ?Hm ?(ltn_ord i) // map_id. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype bigop matrix) CoqEAL(hrel param refinements seqmx seqpoly) Equivalence RelationClasses Morphisms