proposition: Lemma leb_trans : Transitive leb.
proof: Proof. intros x y z. rewrite !leb_le, !le_lteq. intros [Hxy|Hxy] [Hyz|Hyz]. - left; transitivity y; auto. - left; rewrite <- Hyz; auto. - left; rewrite Hxy; auto. - right; transitivity y; auto. Qed.
imports: Relations Morphisms Setoid Equalities