proposition: Lemma Cfpol_root : forall a b c delta, ((delta = b^2 - 4*a * c) -> delta >= 0 -> a <> 0 -> exists x, a * x ^ 2 + b * x + c = 0)%R.
proof: Proof. intros a b c delta Hdelta deltapos Ha. destruct deltapos. destruct (Cpol_2_real_delta_pos a b c delta) as [x H0]. assumption. assumption. assumption. destruct H0 as (x1, H0). exists (-x1)%R. rewrite H0. ring. destruct (Cpol_2_real_delta_eq_0 a b c delta) as [x2 H5]. assumption. assumption. assumption. destruct H5 as (x1, H0). exists (-x1)%R. rewrite H0. ring. Qed.
imports: Complex Cpow_plus