proposition: Lemma nth_R_lt (T1 T2 : Type) (T_R : T1 -> T2 -> Type) x01 x02 s1 s2 : list_R T_R s1 s2 -> forall n, (n < size s1)%N -> T_R (nth x01 s1 n) (nth x02 s2 n).
proof: Proof. move=> Hs n; elim: n s1 s2 Hs=> [|n IH] s1 s2 Hs Hn /=. { by move: Hs Hn; case s1=> [//|h1 t1] Hs _; inversion Hs. } move: Hs Hn IH; case s1=> [//|h1 t1] Hs Hn IH. by inversion Hs; apply IH. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype bigop matrix) CoqEAL(hrel param refinements seqmx seqpoly) Equivalence RelationClasses Morphisms