proposition: Lemma nth_base (s : seq A) k1 k2 i : i < size s -> nth k1 s i = nth k2 s i.
proof: Proof. elim: s i=>[|x xs IH] //= i K; rewrite !nth_cons. by case: eqP=>//; case: i K=>// i; rewrite ltnS=>/IH ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)