proposition: Lemma onth_insert : forall n v p, onth n p = Some v -> exists q r, p = q ++ v :: r.
proof: Proof. intros n v p Hp. set (f := fix aux n (q : list T) := match n, q with | O, _ => nil | S n, nil => nil | S n, h :: t => h :: aux n t end). set (g := fix aux n (q : list T) := match q, n with | nil, _ => nil | h :: t, O => t | h :: t, S n => aux n t end). exists (f n p), (g n p). revert p Hp. induction n as [|n IH] ; simpl ; intros [|h p] Hp ; try easy ; clearbody f g. now injection Hp as ->. simpl. apply f_equal. now apply IH. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)