diff options
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/Binomial.v | 7 | ||||
| -rw-r--r-- | theories/Reals/Rlimit.v | 2 |
2 files changed, 5 insertions, 4 deletions
diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index ad076c488..16f2661fe 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -172,13 +172,12 @@ Proof. apply sum_eq. intros; apply H1. unfold N; apply le_lt_trans with n; [ assumption | apply lt_n_Sn ]. - intros; unfold Bn, Cn. - replace (S N - S i)%nat with (N - i)%nat; reflexivity. + reflexivity. unfold An; fold N; rewrite <- minus_n_n; rewrite H0; simpl; ring. apply sum_eq. - intros; unfold An, Bn; replace (S N - S i)%nat with (N - i)%nat; - [ idtac | reflexivity ]. + intros; unfold An, Bn. + change (S N - S i)%nat with (N - i)%nat. rewrite <- pascal; [ ring | apply le_lt_trans with n; [ assumption | unfold N; apply lt_n_Sn ] ]. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 375cc2752..cf7b91af8 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -174,6 +174,8 @@ Definition limit_in (X X':Metric_Space) (f:Base X -> Base X') Definition R_met : Metric_Space := Build_Metric_Space R R_dist R_dist_pos R_dist_sym R_dist_refl R_dist_tri. +Declare Equivalent Keys dist R_dist. + (*******************************) (** * Limit 1 arg *) (*******************************) |