proposition: Lemma equiv_le_def : forall x y:X, x == y <-> (x <= y /\ y <= x).
proof: Proof. Proof (po_equiv_le_def (po_proof X)). Lemma le_refl : forall x:X, x <= x. Proof (po_le_refl (po_proof X)). Lemma le_trans : forall x y z : X, x <= y -> y <= z -> x <= z. Proof (po_le_trans (po_proof X)). Lemma monotone_def : forall f, monotone X f <-> (forall x y, x <= y -> (f x) <= (f y)). Proof (po_monotone_def (po_proof X)). Lemma antitone_def : forall f, antitone X f <-> (forall x y, x <= y -> (f y) <= (f x)). Proof (po_antitone_def (po_proof X)). Lemma le_equiv_refl : forall x y:X, x == y -> x <= y. Proof. firstorder using equiv_le_def. Qed.
imports: CoRN.algebra.RSetoid