proposition: Lemma gtb_compat : forall p, Proper (eqke==>eq) (gtb p).
proof: Proof. red; intros (x,e) (a,e') (b,e'') H; red in H; simpl in *; destruct H. generalize (gtb_1 (x,e) (a,e'))(gtb_1 (x,e) (b,e'')); destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); auto. - unfold O.ltk in *; simpl in *; intros. symmetry; rewrite H2. apply ME.eq_lt with a; auto with ordered_type. rewrite <- H1; auto. - unfold O.ltk in *; simpl in *; intros. rewrite H1. apply ME.eq_lt with b; auto. rewrite <- H2; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface