proposition: Lemma Cpol_2_real_delta_eq_neg : forall a b c delta, ((delta = b^2 - 4*a * c) -> delta < 0 -> a <> 0 -> ~ (exists x1, exists x2, forall x, a * x ^ 2 + b * x + c = a * (x + x1) * (x + x2)))%R.
proof: Proof. intros a b c delta deltadef Hdelta Ha. destruct (Cpol_d_2 (a +i 0%R) (b +i 0%R) (c +i 0%R) (delta +i 0%R)) as [x1 [x2 H1]]. CusingR2. ring. ring. CusingR2. reflexivity. CusingR2. reflexivity. CusingR2. reflexivity. CusingR2. reflexivity. intro H. destruct H as (x3, H) . destruct H as (x4, H). assert (forall x : C, (a +i 0%R) * x ^ 2 + (b +i 0%R) * x + (c +i 0%R) = (a +i 0%R) * (x + x1) * (x + x2)). intro x. generalize (H1 x). intros H0. destruct H0 as [H2 [H3 [H4 H5]]]. apply H2. assert (H10 : forall x : C, (a +i 0%R) * x ^ 2 + (b +i 0%R) * x + (c +i 0%R) = (a +i 0%R) * (x + (x3 +i 0%R)) * (x + (x4 +i 0%R))). intros x. destruct x as (r, r0). rewrite <- Ceq. split. simpl. ring_simplify. generalize (H r). intro H15. ring_simplify in H15. replace (a * r ^ 2 - a * r0 ^ 2 + r * b + c)%R with ((a * r ^ 2 + r * b + c) - a* r0^2)%R by ring. rewrite H15. ring. simpl. ring_simplify. generalize (H 1%R). intro H15. ring_simplify in H15. generalize (H 0%R). intro H16. ring_simplify in H16. rewrite <- H16 in H15. ring_simplify in H15. rewrite <- Rmult_plus_distr_l in H15. rewrite Rplus_comm in H15. symmetry in H15. rewrite Rplus_comm in H15. apply Rplus_eq_reg_l in H15. rewrite Rplus_comm in H15. apply Rplus_eq_reg_l in H15. rewrite <- H15. ring. assert (Htra : (x1 = (x3 +i 0%R) /\ x2 = (x4 +i 0%R) \/ x1 = (x4 +i 0%R) /\ x2 = (x3 +i 0%R))). assert (forall x : C, (x + (x3 +i 0%R)) * (x + (x4 +i 0%R)) = (x + x1) * (x + x2)). intro x; apply Cmult_eq_reg_l with (a +i 0%R). red; injection 1; auto. generalize (H0 x) (H10 x); intros abs1 abs2. ring_simplify in abs1 ; ring_simplify in abs2 ; ring_simplify. rewrite <- abs1. rewrite abs2. reflexivity. apply Cpol_2_root_unicity. intros x. rewrite H2. reflexivity. generalize (H1 0). intros Hdeltas. destruct Hdeltas as [H2 [H3 [H4 H5]]]. clear H3 H5 H2. assert (Habss : (Cim x1 <> 0%R /\ Cim x2 <> 0%R)). apply H4. intuition. clear H4. destruct Habss as (Habss1, Habss2). destruct Htra as [[Htra1 Htra2]|[Htra1 Htra2]]. rewrite <- Ceq in Htra1. destruct Htra1 as (Htra1, Htraabs). simpl in Htraabs. apply Habss1. assumption. rewrite <- Ceq in Htra1. destruct Htra1 as (Htra1, Htraabs). simpl in Htraabs. apply Habss1. assumption. Qed.
imports: Complex Cpow_plus