proposition: Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, equal cmp m m' = true -> Equivb cmp m m'.
proof: Proof. Proof with auto with ordered_type. intros m Hm m' Hm' cmp; revert m' Hm'. induction Hm as [|[a e] m Hm IHHm Hr]; simpl in *; intros [|[a' e'] m'] Hm' H; try congruence. + split; [tauto|inversion 1]. + destruct X.compare as [?|Heq|?]; try congruence. apply Sorted_inv in Hm'; destruct Hm' as [Hm' Hr']. apply andb_true_iff in H; destruct H as [Hc He]; split. - intros k; split; intros [v Hk]; apply InA_cons in Hk; destruct Hk as [Hk|Hk]. * exists e'; apply InA_cons_hd; split; [|reflexivity]. transitivity a; [apply Hk|apply Heq]. * assert (Hi : In k m'). { apply (IHHm m' Hm' He); exists v; apply Hk. } destruct Hi as [w Hw]; exists w; apply InA_cons_tl, Hw. * exists e; apply InA_cons_hd; split; [|reflexivity]. transitivity a'; [apply Hk|symmetry; apply Heq]. * assert (Hi : In k m). { apply (IHHm m' Hm' He); exists v; apply Hk. } destruct Hi as [w Hw]; exists w; apply InA_cons_tl, Hw. - intros k e1 e2 He1 He2. apply InA_cons in He1, He2. destruct He1 as [He1|He1]; destruct He2 as [He2|He2]. * replace e1 with e by (symmetry; apply He1). replace e2 with e' by (symmetry; apply He2). apply Hc. * assert (Hi : In k m). { apply (IHHm m' Hm' He); exists e2; apply He2. } destruct Hi as [w Hw]. apply InA_eqke_eqk, (Sort_Inf_In Hm Hr) in Hw. destruct He1 as [He1 _]. elim (eq_not_gt He1); apply Hw. * assert (Hi : In k m'). { apply (IHHm m' Hm' He); exists e1; apply He1. } destruct Hi as [w Hw]. apply InA_eqke_eqk, (Sort_Inf_In Hm' Hr') in Hw. destruct He2 as [He2 _]. elim (eq_not_gt He2); apply Hw. * destruct (IHHm m' Hm' He) as [_ IH]. apply (IH k e1 e2 He1 He2). Qed.
imports: FMapInterface