proposition: Lemma RseqmxC_fun_of_seqmx m1 m2 (rm : nat_R m1 m2) n1 n2 (rn : nat_R n1 n2) : refines (RseqmxC rAC rm rn ==> Rord rm ==> Rord rn ==> rAC) ((@fun_of_matrix A m1 n1) : matrix A m1 n1 -> ordinal m1 -> ordinal n1 -> A) (@fun_of_seqmx C _ m2 n2).
proof: Proof. rewrite refinesE => _ a' [_ [[a a'' h1 h2 h3] ra'']] i i' ri j j' rj. rewrite h3 /fun_of_seqmx -ri -rj. apply nth_R_lt. { apply nth_R_lt=>//; rewrite h1 -(nat_R_eq rm); apply ltn_ord. } rewrite h2 -?(nat_R_eq rm) -?(nat_R_eq rn); apply ltn_ord. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype bigop matrix) CoqEAL(hrel param refinements seqmx seqpoly) Equivalence RelationClasses Morphisms