proposition: Lemma max_elt_Above : forall m x e, max_elt m = Some (x,e) -> Above x (remove x m).
proof: Proof. red; intros. rewrite remove_in_iff in H0. destruct H0. rewrite elements_in_iff in H1. destruct H1. unfold max_elt in *. generalize (elements_3 m). revert x e H y x0 H0 H1. induction (elements m). - simpl; intros; try discriminate. - intros. destruct a; destruct l; simpl in *. + injection H as [= -> ->]. inversion_clear H1. * red in H; simpl in *; intuition. elim H0; eauto with ordered_type. * inversion H. + change (max_elt_aux (p::l) = Some (x,e)) in H. generalize (IHl x e H); clear IHl; intros IHl. inversion_clear H1; [ | inversion_clear H2; eauto ]. red in H3; simpl in H3; destruct H3. destruct p as (p1,p2). destruct (E.eq_dec p1 x) as [Heq|Hneq]. * apply ME.lt_eq with p1; auto. inversion_clear H2. inversion_clear H5. red in H2; simpl in H2; ME.order. * apply E.lt_trans with p1; auto. -- inversion_clear H2. inversion_clear H5. red in H2; simpl in H2; ME.order. -- eapply IHl; eauto with ordered_type. ++ econstructor; eauto. red; eauto with ordered_type. ++ inversion H2; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface