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