diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-07 13:37:07 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-07 13:37:07 +0000 |
| commit | faab0757c46bce56fdd2d6908ad63d3bb1889253 (patch) | |
| tree | 88bcc224bb04cbb80e917ec8b9dd98afb5263057 /theories/Reals/R_sqr.v | |
| parent | 0698a5217b372182d39f239c5c8e4b126fb20f46 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2279 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/R_sqr.v')
| -rw-r--r-- | theories/Reals/R_sqr.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 19ac6d97b..c6596c588 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -49,6 +49,14 @@ Lemma Rsqr_eq_0 : (x:R) ``(Rsqr x)==0`` -> ``x==0``. Unfold Rsqr; Intros; Generalize (without_div_Od x x H); Intro; Elim H0; Intro ; Assumption. Save. +Lemma Rsqr_minus_plus : (a,b:R) ``(a-b)*(a+b)==(Rsqr a)-(Rsqr b)``. +Intros; SqRing. +Save. + +Lemma Rsqr_plus_minus : (a,b:R) ``(a+b)*(a-b)==(Rsqr a)-(Rsqr b)``. +Intros; SqRing. +Save. + Lemma Rsqr_incr_0 : (x,y:R) ``(Rsqr x)<=(Rsqr y)`` -> ``0<=x`` -> ``0<=y`` -> ``x<=y``. Intros; Case (total_order_Rle x y); Intro; [Assumption | Cut ``y<x``; [Intro; Unfold Rsqr in H; Generalize (Rmult_lt2 y x y x H1 H1 H2 H2); Intro; Generalize (Rle_lt_trans ``x*x`` ``y*y`` ``x*x`` H H3); Intro; Elim (Rlt_antirefl ``x*x`` H4) | Auto with real]]. Save. |