diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Reals/Rtrigo_alt.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 4815028c0e..5cdfd96ce5 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -219,7 +219,7 @@ Apply pow_lt; Assumption. Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H8 := (sym_eq ? ? ? H7); Elim (fact_neq_0 ? H8). Clear Un Vn; Apply INR_le; Simpl. Induction M_nat. -Assert H6 := (archimed (Rabsolu x)); Elim H6; Intros; Fold M in H6. +Assert H6 := (archimed (Rabsolu x)); Fold M in H6; Elim H6; Intros. Rewrite H4 in H7; Rewrite <- INR_IZR_INZ in H7. Simpl in H7; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H2 H7)). Replace R1 with (INR (S O)); [Apply le_INR | Reflexivity]; Apply le_n_S; Apply le_O_n. @@ -515,4 +515,4 @@ Left; Assumption. Rewrite <- (Ropp_Ropp ``PI/2``); Apply Rle_Ropp1; Unfold Rdiv; Unfold Rdiv in H0; Rewrite <- Ropp_mul1; Exact H0. Intros; Unfold cos_approx; Apply sum_eq; Intros; Unfold cos_term; Do 2 Rewrite pow_Rsqr; Rewrite Rsqr_neg; Unfold Rdiv; Reflexivity. Apply Rgt_RO_Ropp; Assumption. -Qed.
\ No newline at end of file +Qed. |