proposition: Lemma inequality3 : forall x : OF, [--](x[^]2)[-]x[-]Two[<]x.
proof: Proof. intros. apply inv_cancel_less. apply plus_cancel_less with (z := x). simpl in |- *. rstepr ((x[+][1])[*](x[+][1])[+][1]). astepl ([0]:OF). 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