proposition: Lemma nth_map : forall (A : Type) (F : A -> A) (d : A) (l : list A) (i : nat), i < length l -> nth i (map F l) d = F (nth i l d).
proof: Proof. intros; revert i H; induction l; intros; [ inversion H |]; destruct i; simpl; [ reflexivity |]; apply IHl; apply Nat.succ_lt_mono in H; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)