proposition: Lemma Rsqr_sol_eq_0_1 : forall (a:nonzeroreal) (b c x:R), Delta_is_pos a b c -> x = sol_x1 a b c \/ x = sol_x2 a b c -> a * Rsqr x + b * x + c = 0.
proof: Proof. intros; elim H0; intro. - rewrite H1. unfold sol_x1, Delta, Rsqr. field_simplify. + rewrite <- (Rsqr_pow2 (sqrt _)), Rsqr_sqrt. * field. apply a. * apply H. + apply a. - rewrite H1. unfold sol_x2, Delta, Rsqr. field_simplify. + rewrite <- (Rsqr_pow2 (sqrt _)), Rsqr_sqrt. * field. apply a. * apply H. + apply a. Qed.
imports: Rbase Rfunctions Rsqrt_def