diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:30:04 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:30:04 +0000 |
| commit | 096310efb4266fe89455d473f704ec6c7ed5a97c (patch) | |
| tree | 17a6ed5acd135748f43ecb944e268657731a55a2 /theories/Reals/Rtrigo_reg.v | |
| parent | cb7cf50289fbf1c5fe60fd915f63128c88dc6d68 (diff) | |
Renommages dans Rtrigo_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3589 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_reg.v')
| -rw-r--r-- | theories/Reals/Rtrigo_reg.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index 620035ceb..7694cf0a2 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -232,7 +232,7 @@ Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rsqr_pos_lt Assert H0 := (cond_pos r); Red; Intro; Rewrite H1 in H0; Elim (Rlt_antirefl ? H0). Qed. -(* (sin h)/h -> 1 quand h -> 0 *) +(* (sin h)/h -> 1 when h -> 0 *) Lemma derivable_pt_lim_sin_0 : (derivable_pt_lim sin R0 R1). Unfold derivable_pt_lim; Intros. Pose fn := [N:nat][x:R]``(pow ( -1) N)/(INR (fact (plus (mult (S (S O)) N) (S O))))*(pow x (mult (S (S O)) N))``. @@ -298,7 +298,7 @@ Apply (CVN_R_CVS ? X). Apply CVN_R_sin; Unfold fn; Reflexivity. Qed. -(* ((cos h)-1)/h -> 0 quand h -> 0 *) +(* ((cos h)-1)/h -> 0 when h -> 0 *) Lemma derivable_pt_lim_cos_0 : (derivable_pt_lim cos ``0`` ``0``). Unfold derivable_pt_lim; Intros. Assert H0 := derivable_pt_lim_sin_0. |