proposition: Lemma remove_1 : forall m (Hm:Sort m) x y, eq x y -> ~ In y (remove x m).
proof: Proof. intros m Hm x y; generalize Hm; clear Hm. functional induction (remove x m);simpl;intros;subst. red; inversion 1; inversion H0. apply Sort_Inf_NotIn with x0; auto. clear e0. inversion Hm. subst. apply Sort_Inf_NotIn with x0; auto. clear e0;inversion_clear Hm. assert (notin:~ In y (remove y l)) by auto. intros (x1,abs). inversion_clear abs. compute in H1; destruct H1. subst. apply lt_not_eq in _x; now contradict _x. apply notin; exists x1; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses