proposition: Lemma Cpol_2_real_delta_pos : 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. exists (Cre x1). exists (Cre x2). assert (HRtoC : (forall x, Cre ((a +i 0%R) * (x +i 0%R) ^ 2 + (b +i 0%R) * (x +i 0%R) + (c +i 0%R)) = Cre ((a +i 0%R) * ((x +i 0%R) + x1) * ((x +i 0%R) + x2)))). intros x. apply Cre_eq_compat. generalize (H1 (x +i 0%R)). intro H0. destruct H0 as [H2 [H3 [H4 H5]]]. apply H2. intros x. generalize (H1 (x +i 0%R)). intro H0. destruct H0 as [H2 [H3 [H4 H5]]]. assert (HCroot : (Cim x1 = 0%R /\ Cim x2 = 0%R)). apply H3. simpl. split. reflexivity. assumption. CusingR2. ring_simpl. assumption. Qed.
imports: Complex Cpow_plus