aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rtrigo_def.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/Rtrigo_def.v')
-rw-r--r--theories/Reals/Rtrigo_def.v34
1 files changed, 14 insertions, 20 deletions
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index 0d2a9a8ba..b46df202e 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -157,7 +157,7 @@ Proof.
apply Rinv_0_lt_compat; assumption.
rewrite H3 in H0; assumption.
apply lt_le_trans with 1%nat; [ apply lt_O_Sn | apply le_max_r ].
- apply le_IZR; replace (IZR 0) with 0; [ idtac | reflexivity ]; left;
+ apply le_IZR; left;
apply Rlt_trans with (/ eps);
[ apply Rinv_0_lt_compat; assumption | assumption ].
assert (H0 := archimed (/ eps)).
@@ -194,30 +194,27 @@ Proof.
elim H1; intros; assumption.
apply lt_le_trans with (S n).
unfold ge in H2; apply le_lt_n_Sm; assumption.
- replace (2 * n + 1)%nat with (S (2 * n)); [ idtac | ring ].
+ replace (2 * n + 1)%nat with (S (2 * n)) by ring.
apply le_n_S; apply le_n_2n.
apply Rmult_lt_reg_l with (INR (2 * S n)).
apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n))).
apply lt_O_Sn.
- replace (S n) with (n + 1)%nat; [ idtac | ring ].
+ replace (S n) with (n + 1)%nat by ring.
ring.
rewrite <- Rinv_r_sym.
- rewrite Rmult_1_r; replace 1 with (INR 1); [ apply lt_INR | reflexivity ].
+ rewrite Rmult_1_r.
+ apply (lt_INR 1).
replace (2 * S n)%nat with (S (S (2 * n))).
apply lt_n_S; apply lt_O_Sn.
- replace (S n) with (n + 1)%nat; [ ring | ring ].
+ ring.
apply not_O_INR; discriminate.
apply not_O_INR; discriminate.
replace (2 * n + 1)%nat with (S (2 * n));
[ apply not_O_INR; discriminate | ring ].
apply Rle_ge; left; apply Rinv_0_lt_compat.
apply lt_INR_0.
- replace (2 * S n * (2 * n + 1))%nat with (S (S (4 * (n * n) + 6 * n))).
+ replace (2 * S n * (2 * n + 1))%nat with (2 + (4 * (n * n) + 6 * n))%nat by ring.
apply lt_O_Sn.
- apply INR_eq.
- repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR;
- rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR;
- replace (INR 0) with 0; [ ring | reflexivity ].
Qed.
Lemma cosn_no_R0 : forall n:nat, cos_n n <> 0.
@@ -318,28 +315,25 @@ Proof.
elim H1; intros; assumption.
apply lt_le_trans with (S n).
unfold ge in H2; apply le_lt_n_Sm; assumption.
- replace (2 * S n + 1)%nat with (S (2 * S n)); [ idtac | ring ].
+ replace (2 * S n + 1)%nat with (S (2 * S n)) by ring.
apply le_S; apply le_n_2n.
apply Rmult_lt_reg_l with (INR (2 * S n)).
apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n)));
- [ apply lt_O_Sn | replace (S n) with (n + 1)%nat; [ idtac | ring ]; ring ].
+ [ apply lt_O_Sn | ring ].
rewrite <- Rinv_r_sym.
- rewrite Rmult_1_r; replace 1 with (INR 1); [ apply lt_INR | reflexivity ].
+ rewrite Rmult_1_r.
+ apply (lt_INR 1).
replace (2 * S n)%nat with (S (S (2 * n))).
apply lt_n_S; apply lt_O_Sn.
- replace (S n) with (n + 1)%nat; [ ring | ring ].
+ ring.
apply not_O_INR; discriminate.
apply not_O_INR; discriminate.
apply not_O_INR; discriminate.
- left; change (0 < / INR ((2 * S n + 1) * (2 * S n)));
- apply Rinv_0_lt_compat.
+ left; apply Rinv_0_lt_compat.
apply lt_INR_0.
replace ((2 * S n + 1) * (2 * S n))%nat with
- (S (S (S (S (S (S (4 * (n * n) + 10 * n))))))).
+ (6 + (4 * (n * n) + 10 * n))%nat by ring.
apply lt_O_Sn.
- apply INR_eq; repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR;
- rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR;
- replace (INR 0) with 0; [ ring | reflexivity ].
Qed.
Lemma sin_no_R0 : forall n:nat, sin_n n <> 0.