proposition: Lemma Pos_poly_del : forall a b c : R, a <> 0%R -> a > 0%R -> (forall x, 0 <= a*x*x+b*x+c) -> b^2 - 4*a*c <=0.
proof: Proof. intros a b c Ha Haa Hpoly. pose ( b^2 - 4*a*c)%R as delta. destruct (total_order_T delta 0) as [[H|H]|H]. intuition. intuition. destruct (Cfpol_root a b c delta). reflexivity. intuition. assumption. assert (H1 : (exists x1, exists x2, forall x, a * x ^ 2 + b * x + c = a * (x + x1) * (x + x2))%R). apply Cpol_2_real_delta_pos with delta. ring_simplify. reflexivity. assumption. assumption. destruct H1 as [x1 [x2 H1]]. assert (H9 : (0 > a * ( -(x1 + x2)/2 + x1) * ( - (x1 + x2)/2 + x2))%R). replace ((- (x1 + x2) / 2 + x1))%R with ((x1 - x2) /2)%R by field. replace ((- (x1 + x2) / 2 + x2))%R with (-(x1 - x2) /2)%R by field. replace (a * ((x1 - x2) / 2) * (- (x1 - x2) / 2))%R with ( ((x1 - x2) / 2)^2 * (-a))%R by field. replace 0%R with ( ((x1 - x2) / 2) ^ 2 * 0 )%R by ring. apply Rmult_gt_compat_l. assert (H10 : (x1 <> x2)). intro H11. rewrite H11 in H1. assert ((a * 0 ^ 2 + b * 0 + c)%R = (a * (0 + x2) * (0 + x2)))%R. apply H1. assert ((a * 1 ^ 2 + b * 1 + c)%R = (a * (1 + x2) * (1 + x2)))%R. apply H1. ring_simpl. rewrite <- H2 in H3. unfold delta in H. replace (a + b + c)%R with (c + a + b)%R in H3 by ring. replace (c + 2 * a * x2 +a)%R with (c + a + 2 * a * x2)%R in H3 by ring. apply Rplus_eq_reg_l in H3. subst. replace ((2 * a * x2) ^ 2 - 4 * a * (a * x2 ^ 2))%R with (0)%R in H by ring . lra. replace (((x1 - x2) / 2) ^ 2)%R with (Rsqr (((x1 - x2) / 2))) by (unfold Rsqr ; simpl ; ring). apply Rlt_0_sqr. intro H30. replace 0%R with (0/2)%R in H30 by field. unfold Rdiv in *. rewrite Rmult_comm in H30. symmetry in H30. rewrite Rmult_comm in H30. apply Rmult_eq_reg_l in H30. apply H10. symmetry in H30. auto with *. apply Rinv_neq_0_compat. discrR. intuition. assert ( 0 <= a * (- (x1 + x2) / 2 + x1) * (- (x1 + x2) / 2 + x2)). rewrite <- H1. replace ( (- (x1 + x2) / 2) ^ 2)%R with ((- (x1 + x2) / 2) * (- (x1 + x2) / 2) )%R by ring. rewrite <- Rmult_assoc. apply Hpoly. lra. Qed.
imports: Complex Cpow_plus