proposition: Lemma Croot_sqrt_pos : forall a b : R, 0 <= (sqrt (a * a + b * b) - a) / 2.
proof: Proof. intros. unfold Rdiv. replace 0%R with (0 * /2)%R by field. apply Rmult_le_compat_r. lra. apply Rle_Rminus. apply Rle_trans with (Rabs a). split_Rabs. lra. intuition. apply Rsqr_incr_0_var. rewrite Rsqr_sqrt. rewrite <- Rsqr_abs. replace (Rsqr a) with (a * a)%R by intuition. replace (a * a)%R with ((a * a) + 0)%R by intuition. rewrite Rplus_assoc. apply Rplus_le_compat_l. replace (0 + b * b)%R with (Rsqr b) by intuition. intuition. apply (Cnorm_sqr_pos a b). apply sqrt_positivity. apply (Cnorm_sqr_pos a b). Qed.
imports: Complex Cpow_plus