proposition: Lemma inequality4 : forall x : OF, [--](x[^]2)[-]x[-]Two[<]([0]:OF).
proof: Proof. intros. apply inv_cancel_less. astepl ([0]:OF). apply less_wdr with (y := (x[+][1] [/]TwoNZ)[^]2[+](Three [/]FourNZ[+][1])). apply less_leEq_trans with (y := Three [/]FourNZ[+]([1]:OF)). apply plus_resp_pos. apply div_resp_pos. apply pos_four. apply pos_three. apply pos_one. apply plus_cancel_leEq_rht with (z := [--](Three [/]FourNZ[+]([1]:OF))). astepl ([0]:OF). rstepr ((x[+]([1]:OF) [/]TwoNZ)[^]2). apply sqr_nonneg. simpl in |- *. rational. Qed.
imports: CoRN.reals.Bridges_LUB