proposition: Lemma min_elt_Below : forall m x e, min_elt m = Some (x,e) -> Below x (remove x m).
proof: Proof. unfold min_elt, Below; intros. rewrite remove_in_iff in H0; destruct H0. rewrite elements_in_iff in H1. destruct H1. generalize (elements_3 m). destruct (elements m). - try discriminate. - destruct p; injection H as [= -> ->]; intros H4. inversion_clear H1 as [? ? H2|? ? H2]. + red in H2; destruct H2; simpl in *; ME.order. + inversion_clear H4. rename H1 into H3. rewrite (@InfA_alt _ eqke) in H3 by auto with typeclass_instances. apply (H3 (y,x0)); auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface