diff options
author | 2014-09-23 13:11:24 +0200 | |
---|---|---|
committer | 2014-09-23 13:11:24 +0200 | |
commit | 13ab2df9ed3a5ea6b7455ea8a7da4341e7f2bcd5 (patch) | |
tree | fd42f041d099700403dfc0a3af69ea5791ec5930 /theories/Reals/Rfunctions.v | |
parent | 85355cfda7a01fa532f111ee7c4d522a8be8a399 (diff) |
adds general facts in the Reals library, whose need was detected in
experiments about computing PI
Diffstat (limited to 'theories/Reals/Rfunctions.v')
-rw-r--r-- | theories/Reals/Rfunctions.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 9beee06c5..6e9a34ab4 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -520,6 +520,12 @@ Proof. apply Rle_trans with (Rabs y); [ apply Rabs_pos | exact H ]. Qed. +Lemma Rsqr_pow2 : forall x, Rsqr x = x ^ 2. +Proof. +intros; unfold Rsqr; simpl; rewrite Rmult_1_r; reflexivity. +Qed. + + (*******************************) (** * PowerRZ *) (*******************************) @@ -783,6 +789,13 @@ Proof. ring. Qed. +Lemma R_dist_mult_l : forall a b c, + R_dist (a * b) (a * c) = Rabs a * R_dist b c. +Proof. +unfold R_dist. +intros a b c; rewrite <- Rmult_minus_distr_l, Rabs_mult; reflexivity. +Qed. + (*******************************) (** * Infinite Sum *) (*******************************) |