diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-05 15:02:47 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-05 15:02:47 +0000 |
| commit | 464def74f4f0ea69029adf5cb6ef51d57faaec3b (patch) | |
| tree | b9d2cfc8dce60f34c5d6c314d6136593a044a950 /theories/Reals/R_sqr.v | |
| parent | e52b55b2e60a38f61b0fd6b161e081e825bcf8be (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2270 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, 4 insertions, 0 deletions
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 39cca741c..19ac6d97b 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -37,6 +37,10 @@ Lemma Rsqr_gt_0_0 : (x:R) ``0<(Rsqr x)`` -> ~``x==0``. Intros; Red; Intro; Rewrite H0 in H; Rewrite Rsqr_O in H; Elim (Rlt_antirefl ``0`` H). Save. +Lemma Rsqr_pos_lt : (x:R) ~(x==R0)->``0<(Rsqr x)``. +Intros; Case (total_order R0 x); Intro; [Unfold Rsqr; Apply Rmult_lt_pos; Assumption | Elim H0; Intro; [Elim H; Symmetry; Exact H1 | Rewrite Rsqr_neg; Generalize (Rlt_Ropp x ``0`` H1); Rewrite Ropp_O; Intro; Unfold Rsqr; Apply Rmult_lt_pos; Assumption]]. +Save. + Lemma Rsqr_div : (x,y:R) ~``y==0`` -> ``(Rsqr (x/y))==(Rsqr x)/(Rsqr y)``. Intros; Unfold Rsqr; Field; Repeat Apply prod_neq_R0; Assumption. Save. |