proposition: Lemma leEq_geEq : forall x y : OF, (forall t : OF, t[<]x -> t[<]y) -> forall z : OF, y[<]z -> x[<]z.
proof: Proof. intros x y H z H0. apply plus_cancel_less with (z := [--](z[-]y)). rstepr y. apply H. apply shift_plus_less. apply plus_cancel_less with (z := [--]x). rstepr (z[-]y). astepl ([0]:OF). apply shift_zero_less_minus. assumption. Qed.
imports: CoRN.reals.Bridges_LUB