proposition: Lemma Rsqr_sol_eq_0_0 : forall (a:nonzeroreal) (b c x:R), Delta_is_pos a b c -> a * Rsqr x + b * x + c = 0 -> x = sol_x1 a b c \/ x = sol_x2 a b c.
proof: Proof. intros; rewrite (canonical_Rsqr a b c x) in H0; rewrite Rplus_comm in H0; generalize (Rplus_opp_r_uniq ((4 * a * c - Rsqr b) / (4 * a)) (a * Rsqr (x + b / (2 * a))) H0); assert (Rsqr b - 4 * a * c = Delta a b c) by reflexivity. replace (- ((4 * a * c - Rsqr b) / (4 * a))) with ((Rsqr b - 4 * a * c) / (4 * a)). 2:{ unfold Rdiv; rewrite <- Ropp_mult_distr_l_reverse. rewrite Ropp_minus_distr. reflexivity. } rewrite H1; intro; generalize (Rmult_eq_compat_l (/ a) (a * Rsqr (x + b / (2 * a))) (Delta a b c / (4 * a)) H2); replace (/ a * (a * Rsqr (x + b / (2 * a)))) with (Rsqr (x + b / (2 * a))). 2:{ rewrite <- Rmult_assoc; rewrite Rinv_l. - symmetry ; apply Rmult_1_l. - apply (cond_nonzero a). } replace (/ a * (Delta a b c / (4 * a))) with (Rsqr (sqrt (Delta a b c) / (2 * a))). 2:{ rewrite Rsqr_div'. rewrite Rsqr_sqrt. 2:assumption. unfold Rdiv. rewrite (Rmult_comm (/ a)). rewrite Rmult_assoc. rewrite <- Rinv_mult. replace (4 * a * a) with (Rsqr (2 * a)) by ring_Rsqr. reflexivity. } intro; generalize (Rsqr_eq (x + b / (2 * a)) (sqrt (Delta a b c) / (2 * a)) H3); intro; elim H4; intro. - left; unfold sol_x1; generalize (Rplus_eq_compat_l (- (b / (2 * a))) (x + b / (2 * a)) (sqrt (Delta a b c) / (2 * a)) H5); replace (- (b / (2 * a)) + (x + b / (2 * a))) with x by ring. intro; rewrite H6; unfold Rdiv; ring. - right; unfold sol_x2; generalize (Rplus_eq_compat_l (- (b / (2 * a))) (x + b / (2 * a)) (- (sqrt (Delta a b c) / (2 * a))) H5); replace (- (b / (2 * a)) + (x + b / (2 * a))) with x by ring. intro; rewrite H6; unfold Rdiv; ring. Qed.
imports: Rbase Rfunctions Rsqrt_def