proposition: Lemma nth_in : forall (A : Type) (s : A) (lh lt : list A), nth_error (lh ++ s :: lt) (length lh) = Some s.
proof: Proof. intros; induction lh; simpl; [ reflexivity | assumption ]. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)