diff options
| -rw-r--r-- | theories/Reals/R_sqr.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index c6596c5883..1dfa67c8db 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -245,7 +245,7 @@ Intros a b c d; Apply Rsqr_incr_0_var; [Rewrite Rsqr_times; Repeat Rewrite Rsqr_ Save. (************************************************************) -(* Resolution of a*X^2+b*X+c=0 *) +(* Resolution of [a*X^2+b*X+c=0] *) (************************************************************) Definition Delta [a:nonzeroreal;b,c:R] : R := ``(Rsqr b)-4*a*c``. @@ -311,4 +311,4 @@ Symmetry; Apply Rmult_1l. Apply (cond_nonzero a). Unfold Rdiv; Field; Case a; Intros y H3; Apply prod_neq_R0; [DiscrR | Assumption]. Unfold Delta; Reflexivity. -Save.
\ No newline at end of file +Save. |