proposition: Lemma notin_remove: forall l x, ~ In x l -> remove x l = l.
proof: Proof. intros l x; induction l as [|y l IHl]; simpl; intros Hnin. - reflexivity. - destruct (eq_dec x y); [subst|f_equal]; tauto. Qed.
imports: PeanoNat