proposition: Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
proof: Proof. intros (m1,Hm1); induction m1; intros (m2, Hm2); destruct m2; intros (m3, Hm3); destruct m3; unfold lt; simpl; try destruct a as (x,e); try destruct p as (x',e'); try destruct p0 as (x'',e''); try contradiction; auto. destruct (X.compare x x') as [Hlt|Heq|Hlt]; destruct (X.compare x' x'') as [Hlt'|Heq'|Hlt']; MapS.Raw.MX.elim_comp; intuition. - left; apply D.lt_trans with e'; auto. - left; apply lt_eq with e'; auto. - left; apply eq_lt with e'; auto. - right. split. + apply D.eq_trans with e'; auto. + inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3. apply (IHm1 H2 (Build_slist H6) (Build_slist H8)); intuition. Qed.
imports: FMapInterface