proposition: Lemma sqrt2_correct (Qsqrt_overapprox: forall (x: QnonNeg) (e: Qpos), { r: QnonNeg | ` x <= ` r * ` r /\ ` r * ` r < ` x + e }%Q): sqrt2 * sqrt2 == (2#1)%Qnn.
proof: Proof. Proof with auto. unfold eq, le. simpl. split; intros. destruct (Qpos_lt_plus H0). destruct (Qsqrt_overapprox (2#1)%Qnn x). destruct a. apply (is_binop_bound Qmult) with x0 x0... rewrite q0. apply Qle_trans with ((2 # 1)%Q + x)%Q... apply Qplus_le_compat... inversion_clear H. destruct (Qlt_le_dec (`q0) (`q')). apply Qle_trans with (`q0*`q0)%Q... apply Qle_trans with (`q0*`q')%Q... apply Qmult_le_compat... apply Qle_trans with (`q)... apply Qle_trans with (`q'*`q')%Q... apply Qle_trans with (`q0*`q')%Q... apply Qmult_le_compat... apply Qle_trans with (`q)... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program