proposition: Lemma leb_le : forall x y, leb x y <-> x <= y.
proof: Proof. intros x y. unfold leb. rewrite le_lteq. destruct (compare_spec x y) as [EQ|LT|GT]; split; auto. - discriminate. - intros LE. elim (StrictOrder_Irreflexive x). destruct LE as [LT|EQ]. + now transitivity y. + now rewrite <- EQ in GT. Qed.
imports: Relations Morphisms Setoid Equalities