proposition: Lemma le_lt_eq {A}{lt: relation A}: forall a b, leq lt a b <-> lt a b \/ a = b.
proof: Proof. split; destruct 1; auto 2. - now left. - subst; now right. Qed.
imports: Coq(RelationClasses Relation_Operators Ensembles Setoid)