proposition: Lemma Croot_pol_2 : forall z : C, {z1 | z1 ^ 2 = z}.
proof: Proof. intros. destruct z as (a, b). destruct (Rlt_le_dec b 0). exists (sqrt ( (sqrt ( a * a + b * b) + a)/2), - sqrt ( (sqrt ( a * a + b * b) - a)/2))%R. CusingR_simpl ; ring_simplify. repeat rewrite sqrt_square2. field. destruct (Croot_sqrt_pos a b). intuition. intuition. destruct (Croot_sqrt_pos_plus a b). intuition. intuition. rewrite Rmult_assoc. rewrite <- sqrt_mult. field_simplify ((sqrt (a * a + b * b) + a) / 2 * ((sqrt (a * a + b * b) - a) / 2))%R. rewrite sqrt_square2. field_simplify ((a * a + b * b - a ^ 2) / 4)%R. unfold Rdiv. replace (/4)%R with (/2 * /2)%R by field. rewrite sqrt_mult. replace (sqrt (/2 * /2))%R with (/2)%R by (rewrite sqrt_square ; try reflexivity ; lra). replace (b ^ 2)%R with (-b * -b)%R by ring. rewrite sqrt_square. field. lra. replace (b ^ 2)%R with (Rsqr b) by (simpl ; rewrite Rmult_1_r ; intuition). intuition. lra. apply Rle_ge . apply (Cnorm_sqr_pos a b). apply Croot_sqrt_pos_plus. apply Croot_sqrt_pos. exists (sqrt ( (sqrt ( a * a + b * b) + a)/2), sqrt ( (sqrt ( a * a + b * b) - a)/2))%R. CusingR_simpl ; ring_simplify. repeat rewrite sqrt_square2. field. apply Rle_ge. apply Croot_sqrt_pos. apply Rle_ge. apply Croot_sqrt_pos_plus. rewrite Rmult_assoc. repeat rewrite <- sqrt_mult. field_simplify ((sqrt (a * a + b * b) + a) / 2 * ((sqrt (a * a + b * b) - a) / 2))%R. repeat rewrite sqrt_square2. field_simplify ((a * a + b * b - a ^ 2) / 4)%R. unfold Rdiv. replace (/4)%R with (/2 * /2)%R by field. rewrite sqrt_mult. replace (sqrt (/2 * /2))%R with (/2)%R by (rewrite sqrt_square ; try reflexivity ; lra). replace (b ^ 2)%R with (b * b)%R by ring. rewrite sqrt_square. field. lra. replace (b ^ 2)%R with (Rsqr b) by (simpl ; rewrite Rmult_1_r ; intuition). intuition. lra. apply Rle_ge . apply (Cnorm_sqr_pos a b). apply Croot_sqrt_pos_plus. apply Croot_sqrt_pos. Qed.
imports: Complex Cpow_plus