proposition: Lemma onth_nth : forall n p d, n < length p -> onth n p = Some (nth n p d).
proof: Proof. induction n as [|n IH] ; intros [|h p] d Hl ; try easy. simpl. apply IH. now rewrite Nat.succ_lt_mono. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)