proposition: Lemma remove_1 : forall m (Hm:Sort m) x y, X.eq x y -> ~ In y (remove x m).
proof: Proof. intros m Hm x y He [e H]; revert e H. induction Hm as [|[a m] l Hm IHHm Hr]; simpl in *; intros e H. - now inversion H. - destruct X.compare as [Hlt|Heq|Hgt]. + apply InA_cons in H; destruct H; [compute in H; destruct H; order|]. apply InA_eqke_eqk in H; apply (Sort_Inf_In Hm Hr) in H. compute in H; order. + apply InA_eqke_eqk in H; apply (Sort_Inf_In Hm Hr) in H. compute in H; order. + apply InA_cons in H; destruct H; [compute in H; destruct H; order|]. apply (IHHm e), H. Qed.
imports: FMapInterface