proposition: Lemma rest_safe : forall ns l i, i < l -> In i (afs_rest ns ns l).
proof: Proof. intros ns; cut (forall l i, i < l -> forall ac, (forall x, In x ns -> In x ac) -> In i (afs_rest ns ac l)); [ intros; apply H; try intros; assumption |]. induction l; intros; simpl; [ inversion H |]; apply Nat.lt_eq_cases in H; destruct H; [ destruct (existsb (Nat.eqb l)); apply IHl; try apply Nat.succ_lt_mono; try assumption; intros; right; apply H0; assumption |]. assert (Hk : forall k ac, In i ac -> In i (afs_rest ns ac k)); [ induction k; intros; simpl; [ assumption |]; destruct (existsb (Nat.eqb k) ns); apply IHk; [| right ]; assumption |]. apply eq_add_S in H; rewrite <- H; clear H IHl; case_eq (existsb (Nat.eqb i) ns); intros; [| apply Hk; left; reflexivity ]. apply existsb_exists in H; destruct H as [j [Hi H]]; apply Nat.eqb_eq in H; rewrite <- H in Hi; clear H; apply Hk; apply H0; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)