diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-21 19:03:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-21 19:03:58 +0000 |
| commit | cf3d8a16556e102b21521bf1b57dc2e43bf06951 (patch) | |
| tree | bee313eef7cb1c964333d373a6448847416cafe3 /theories/Reals/R_sqr.v | |
| parent | 8ca47d88d7dfbec6810ff06d715066a9296b1a4c (diff) | |
Passage coqweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2371 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/R_sqr.v')
| -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 c6596c588..1dfa67c8d 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. |