proposition: Lemma Cpol_d_2 : forall a b c delta, (delta = b^2 - 4*a * c) -> a <> 0 -> Cim a = 0%R -> Cim b = 0%R -> Cim c = 0%R -> exists x1, exists x2, forall x, a * x ^ 2 + b * x + c = a * (x + x1) * (x + x2) /\ ((Cim delta) = 0%R /\ Cre delta > 0%R -> Cim x1 = 0%R /\ Cim x2 = 0%R) /\ ((Cim delta) = 0%R /\ Cre delta < 0%R -> Cim x1 <> 0%R /\ Cim x2 <> 0%R) /\ ((Cim delta) = 0%R /\ Cre delta = 0%R -> x1 = x2 /\ Cim x1 = 0%R).
proof: Proof. intros a b c delta Hdelta Ha Hima Himb Himc. destruct (Croot_pol_2 delta) as [delta1 Hsquare]. exists (( b / (a + a) - delta1 / (a + a))). exists (( b / (a + a) + delta1 / (a + a))). intros x. repeat split. unfold Cdiv. ring_simplify. rewrite Hsquare. rewrite Hdelta. unfold Cminus. repeat rewrite Cadd_assoc. apply Cadd_eq_compat_l. ring_simplify. rewrite Rplus_0_l. assert (H : (2 * 2 = 4)) by (CusingR_simpl ; ring). rewrite <- H. replace ((R1+R1)%R, R0) with (IRC 2) by (reflexivity). replace (a + a) with (2 * a) by (CusingR_simpl ; ring). field. split. assumption. intro H0. rewrite <- Ceq in H0. simpl in H0. destruct H0. assert (2 <> 0)%R by discrR. intuition. CusingR2. ring_simpl. generalize H2. intro H3. (apply Rmult_integral in H3 ; destruct H3 as [H3|H3]). (apply Rmult_integral in H3 ; destruct H3 as [H3|H3]). lra. rewrite H3 in *. rewrite <- H1 in H0. ring_simpl. apply Rpow_2_opp_inf_0 in H0. destruct H0. rewrite H3. ring. CusingR2. ring_simpl. (apply Rmult_integral in H2 ; destruct H2 as [H2|H2]). (apply Rmult_integral in H2 ; destruct H2 as [H2|H2]). lra. rewrite H2 in H1. rewrite <- H1 in H0. ring_simpl. apply Rpow_2_opp_inf_0 in H0. destruct H0. rewrite H2. ring. CusingR2. ring_simpl. apply Rmult_integral in H0 ; destruct H0 as [H0|H0]. apply Rmult_integral in H0 ; destruct H0 as [H0|H0]. apply Rmult_integral in H0 ; destruct H0 as [H0|H0]. lra. apply Rinv_neq_0_compat in H0. destruct H0. intro H8. ring_simplify in H8. apply Rmult_integral in H8. destruct H8 as [H8|H8]. lra. replace (r9 ^ 2)%R with (Rsqr r9) in H8 by (unfold Rsqr ; simpl ; ring). assert (H5 : (r9 = 0)%R). apply Rsqr_0_uniq ; assumption. rewrite H5 in *. apply Ha. split ; reflexivity. assumption. rewrite H0 in *. ring_simpl. rewrite <- H2 in H1. apply Rpow_2_inf_0 in H1. destruct H1. reflexivity. CusingR2. ring_simpl. apply Rmult_integral in H0 ; destruct H0 as [H0|H0]. apply Rmult_integral in H0 ; destruct H0 as [H0|H0]. apply Rmult_integral in H0 ; destruct H0 as [H0|H0]. lra. apply Rinv_neq_0_compat in H0. destruct H0. intro H8. ring_simplify in H8. apply Rmult_integral in H8. destruct H8 as [H8|H8]. lra. replace (r9 ^ 2)%R with (Rsqr r9) in H8 by (unfold Rsqr ; simpl ; ring). assert (H5 : (r9 = 0)%R). apply Rsqr_0_uniq ; assumption. rewrite H5 in *. apply Ha. split ; reflexivity. assumption. rewrite H0 in *. ring_simpl. rewrite <- H2 in H1. apply Rpow_2_inf_0 in H1. destruct H1. reflexivity. unfold Cminus. apply Cadd_eq_compat_l. assert (H0 : (delta = 0)) by (rewrite <- Ceq ; intuition). rewrite H0 in *. assert (H1 : delta1 = 0). simpl in Hsquare. rewrite Cmult_1_r in Hsquare. apply Cmult_integral in Hsquare. destruct Hsquare ; assumption. rewrite H1. unfold Cdiv. ring. CusingR2. ring_simpl. apply Rmult_integral in H2 ; destruct H2 as [H2|H2]. apply Rmult_integral in H2 ; destruct H2 as [H2|H2]. lra. rewrite H2 in *. ring_simplify in H1. rewrite <- H1 in H0. replace (r2 ^ 2)%R with (Rsqr r2) in H0 by (unfold Rsqr ; simpl ; ring). assert (H10 : (r2 = 0)%R). apply Rsqr_0_uniq. apply Ropp_eq_0_compat in H0. ring_simplify in H0. assumption. rewrite H10 in *. ring. rewrite H2 in *. ring. Qed.
imports: Complex Cpow_plus