proposition: Lemma Cpol_pos : forall a b c delta, (delta = b^2 - 4*a * c)%R -> a <> 0%R -> (forall x, 0 <> a*x*x+b*x+c)%R -> delta < 0%R.
proof: Proof. intros a b c delta Hdelta Ha. intro Hpoly. destruct (total_order_T delta 0) as [[H|H]|H]. assumption. destruct (Cfpol_root a b c delta). assumption. intuition. assumption. destruct (Hpoly x). ring_simplify. symmetry. ring_simplify in H0. assumption. destruct (Cfpol_root a b c delta). assumption. intuition. assumption. destruct (Hpoly x). ring_simplify. symmetry. ring_simplify in H0. assumption. Qed.
imports: Complex Cpow_plus