proposition: Lemma inequality1 : forall x : OF, x[<]x[^]2[-]x[+]Two.
proof: Proof. intros. apply plus_cancel_less with (z := [--]x). astepl ([0]:OF). simpl in |- *. rstepr ((x[-][1])[*](x[-][1])[+][1]). apply less_wdr with (y := (x[-][1])[^]2[+]([1]:OF)). apply less_leEq_trans with (y := [1]:OF). apply pos_one. apply plus_cancel_leEq_rht with (z := [--]([1]:OF)). astepl ([0]:OF). rstepr ((x[-]([1]:OF))[^]2). apply sqr_nonneg. simpl in |- *. rational. Qed.
imports: CoRN.reals.Bridges_LUB