proposition: Lemma leb_compat : forall p, Proper (eqke==>eq) (leb p).
proof: Proof. red; intros x a b H. unfold leb; f_equal; apply gtb_compat; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface