diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:37 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:37 +0000 |
commit | ffb64d16132dd80f72ecb619ef87e3eee1fa8bda (patch) | |
tree | 5368562b42af1aeef7e19b4bd897c9fc5655769b /theories/Reals/Rprod.v | |
parent | a46ccd71539257bb55dcddd9ae8510856a5c9a16 (diff) |
Kills the useless tactic annotations "in |- *"
Most of these heavyweight annotations were introduced a long time ago
by the automatic 7.x -> 8.0 translator
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rprod.v')
-rw-r--r-- | theories/Reals/Rprod.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 6bcf4bd4c..e97894af3 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -36,7 +36,7 @@ Proof. replace (S n - k - 1)%nat with O; [rewrite H1; simpl|omega]. replace (n+1+0)%nat with (S n); ring. replace (S n - k-1)%nat with (S (n - k-1));[idtac|omega]. - simpl in |- *; replace (k + S (n - k))%nat with (S n). + simpl; replace (k + S (n - k))%nat with (S n). replace (k + 1 + S (n - k - 1))%nat with (S n). rewrite Hrecn; [ ring | assumption ]. omega. @@ -49,8 +49,8 @@ Lemma prod_SO_pos : (forall n:nat, (n <= N)%nat -> 0 <= An n) -> 0 <= prod_f_R0 An N. Proof. intros; induction N as [| N HrecN]. - simpl in |- *; apply H; trivial. - simpl in |- *; apply Rmult_le_pos. + simpl; apply H; trivial. + simpl; apply Rmult_le_pos. apply HrecN; intros; apply H; apply le_trans with N; [ assumption | apply le_n_Sn ]. apply H; apply le_n. @@ -64,7 +64,7 @@ Lemma prod_SO_Rle : Proof. intros; induction N as [| N HrecN]. elim H with O; trivial. - simpl in |- *; apply Rle_trans with (prod_f_R0 An N * Bn (S N)). + simpl; apply Rle_trans with (prod_f_R0 An N * Bn (S N)). apply Rmult_le_compat_l. apply prod_SO_pos; intros; elim (H n (le_trans _ _ _ H0 (le_n_Sn N))); intros; assumption. @@ -114,7 +114,7 @@ Proof. (if eq_nat_dec n 0 then 1 else INR n) = INR n). intros n; case (eq_nat_dec n 0); auto with real. intros; absurd (0 < n)%nat; omega. - intros; unfold Rsqr in |- *; repeat rewrite fact_prodSO. + intros; unfold Rsqr; repeat rewrite fact_prodSO. cut ((k=N)%nat \/ (k < N)%nat \/ (N < k)%nat). intro H2; elim H2; intro H3. rewrite H3; replace (2*N-N)%nat with N;[right; ring|omega]. @@ -164,14 +164,14 @@ Qed. (**********) Lemma INR_fact_lt_0 : forall n:nat, 0 < INR (fact n). Proof. - intro; apply lt_INR_0; apply neq_O_lt; red in |- *; intro; - elim (fact_neq_0 n); symmetry in |- *; assumption. + intro; apply lt_INR_0; apply neq_O_lt; red; intro; + elim (fact_neq_0 n); symmetry ; assumption. Qed. (** We have the following inequality : (C 2N k) <= (C 2N N) forall k in [|O;2N|] *) Lemma C_maj : forall N k:nat, (k <= 2 * N)%nat -> C (2 * N) k <= C (2 * N) N. Proof. - intros; unfold C in |- *; unfold Rdiv in |- *; apply Rmult_le_compat_l. + intros; unfold C; unfold Rdiv; apply Rmult_le_compat_l. apply pos_INR. replace (2 * N - N)%nat with N. apply Rmult_le_reg_l with (INR (fact N) * INR (fact N)). |