proposition: Lemma onth_app_l : forall n p q, n < length p -> onth n (p ++ q) = onth n p.
proof: Proof. intros n p q. revert n. induction p as [|v p IH]. easy. intros [|n] ; simpl. easy. intros H. rewrite <-Nat.succ_lt_mono in H. now apply IH. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)