proposition: Lemma RseqmxC_spec_seqmx m n (M : @seqmx C) : (size M == m) && all (fun r => size r == n) M -> (list_R (list_R rAC)) (map_seqmx spec M) M -> RseqmxC rAC (nat_Rxx m) (nat_Rxx n) (spec_seqmx m n M) M.
proof: Proof. move=> /andP [] /eqP Hm /all_nthP Hn Hc; apply refinesP. eapply (refines_trans (b:=map_seqmx spec M)); [by tc| |]. { rewrite refinesE; split; [by rewrite size_map| |]. { move=> i Hi; rewrite (nth_map 0%C) ?Hm // size_map. by apply/eqP/Hn; rewrite Hm. } by move=> i j; rewrite mxE. } by rewrite refinesE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype bigop matrix) CoqEAL(hrel param refinements seqmx seqpoly) Equivalence RelationClasses Morphisms