proposition: Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
proof: Proof. intros (m1,Hm1); induction m1; intros (m2, Hm2); destruct m2; unfold eq, lt; simpl; try destruct a as (x,e); try destruct p as (x',e'); try contradiction; auto. destruct (X.compare x x') as [Hlt|Heq|Hlt]; auto. intuition. - exact (D.lt_not_eq H0 H1). - inversion_clear Hm1; inversion_clear Hm2. apply (IHm1 H0 (Build_slist H5)); intuition. Qed.
imports: FMapInterface