From 09f771924e911acd5fb3d2fea8289980d9ea0ec8 Mon Sep 17 00:00:00 2001 From: Ana Dalton Date: Fri, 19 May 2023 21:38:36 -0700 Subject: [PATCH] 'Deprecate Nat.div_le_mono for Div0.div_le_mono' --- reals/stdlib/CMTFullSets.v | 2 +- reals/stdlib/CMTIntegrableFunctions.v | 8 ++++---- reals/stdlib/ConstructiveDiagonal.v | 8 ++++---- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/reals/stdlib/CMTFullSets.v b/reals/stdlib/CMTFullSets.v index f87d83cc..8603622a 100644 --- a/reals/stdlib/CMTFullSets.v +++ b/reals/stdlib/CMTFullSets.v @@ -166,7 +166,7 @@ Proof. destruct xdf as [xnDiag cvDiag]. assert (forall a b:nat, lt a b -> lt (diagPlane n a) (diagPlane n b)). { intros. unfold diagPlane. apply Nat.add_lt_le_mono. assumption. - apply Nat.div_le_mono. auto. apply Nat.mul_le_mono. + apply Nat.Div0.div_le_mono. auto. apply Nat.mul_le_mono. apply Nat.add_le_mono. apply Nat.le_refl. unfold lt in H0. apply (Nat.le_trans _ (S a)). apply le_S. apply Nat.le_refl. assumption. apply le_n_S. apply Nat.add_le_mono. apply Nat.le_refl. unfold lt in H0. diff --git a/reals/stdlib/CMTIntegrableFunctions.v b/reals/stdlib/CMTIntegrableFunctions.v index 82044286..395f1487 100644 --- a/reals/stdlib/CMTIntegrableFunctions.v +++ b/reals/stdlib/CMTIntegrableFunctions.v @@ -434,13 +434,13 @@ Proof. apply (CRle_trans _ _ _ (CRabs_triang _ _)). setoid_replace (1 # n)%Q with ((1 # (2*n)) + (1 # (2*n)))%Q. apply le_S_n in H1. rewrite CR_of_Q_plus. apply CRplus_le_compat. - apply H. rewrite <- (Nat.div_mul N 2). apply Nat.div_le_mono. + apply H. rewrite <- (Nat.div_mul N 2). apply Nat.Div0.div_le_mono. auto. apply (Nat.le_trans (N*2) (N*2 + (S N0)*2)). apply Nat.le_add_r. apply (Nat.le_trans _ i). assumption. apply le_S. apply Nat.le_refl. auto. apply H0. assert (N0 = pred (S N0)). reflexivity. rewrite H2. apply Nat.pred_le_mono. rewrite <- (Nat.div_mul (S N0) 2). - apply Nat.div_le_mono. auto. + apply Nat.Div0.div_le_mono. auto. apply (Nat.le_trans _ (N*2 + (S N0)*2)). rewrite Nat.add_comm. apply Nat.le_add_r. apply (Nat.le_trans (N*2 + (S N0)*2) i). assumption. apply le_S. apply Nat.le_refl. auto. @@ -453,11 +453,11 @@ Proof. apply (CRle_trans _ _ _ (CRabs_triang _ _)). setoid_replace (1 # n)%Q with ((1 # (2*n)) + (1 # (2*n)))%Q. apply le_S_n in H1. rewrite CR_of_Q_plus. apply CRplus_le_compat. - apply H. rewrite <- (Nat.div_mul N 2). apply Nat.div_le_mono. + apply H. rewrite <- (Nat.div_mul N 2). apply Nat.Div0.div_le_mono. auto. apply (Nat.le_trans (N*2) (N*2 + (S N0)*2)). apply Nat.le_add_r. apply (Nat.le_trans _ i). assumption. apply le_S. apply Nat.le_refl. auto. apply H0. rewrite <- (Nat.div_mul N0 2). - apply Nat.div_le_mono. auto. + apply Nat.Div0.div_le_mono. auto. apply (Nat.le_trans (N0*2) (N*2 + (S N0)*2)). rewrite Nat.add_comm. apply (Nat.le_trans (N0 * 2) (S N0 * 2)). apply Nat.mul_le_mono_r. apply le_S. apply Nat.le_refl. diff --git a/reals/stdlib/ConstructiveDiagonal.v b/reals/stdlib/ConstructiveDiagonal.v index 840c8dcb..97b096c0 100644 --- a/reals/stdlib/ConstructiveDiagonal.v +++ b/reals/stdlib/ConstructiveDiagonal.v @@ -285,7 +285,7 @@ Proof. assert (I = K). - destruct (Nat.lt_trichotomy I K). + exfalso. unfold lt in H0. assert ((S I) * S (S I) / 2 <= K * S K / 2)%nat. - apply Nat.div_le_mono. intro absurd. inversion absurd. + apply Nat.Div0.div_le_mono. apply Nat.mul_le_mono_nonneg. apply Nat.le_0_l. assumption. apply Nat.le_0_l. apply le_n_S. assumption. rewrite diagPlaneAbsNext in H1. apply (Nat.add_le_mono_l (I * S I / 2 + S I) (K * S K / 2) l) in H1. @@ -298,7 +298,7 @@ Proof. assumption. apply Nat.le_refl. + destruct H0. assumption. exfalso. unfold lt in H0. assert ((S K) * S (S K) / 2 <= I * S I / 2)%nat. - apply Nat.div_le_mono. intro absurd. inversion absurd. + apply Nat.Div0.div_le_mono. apply Nat.mul_le_mono_nonneg. apply Nat.le_0_l. assumption. apply Nat.le_0_l. apply le_n_S. assumption. rewrite diagPlaneAbsNext in H1. apply (Nat.add_le_mono_l (K * S K / 2 + S K) (I * S I / 2) j) in H1. @@ -433,7 +433,7 @@ Proof. rewrite des in H0. unfold diagPlane in H0. unfold diagPlane. subst p. rewrite Nat.add_0_l. ring. unfold diagPlane. rewrite Nat.add_0_l. rewrite Nat.add_0_l. remember (i + j)%nat. apply Nat.add_le_mono. assumption. - apply Nat.div_le_mono. auto. apply Nat.mul_le_mono_nonneg. + apply Nat.Div0.div_le_mono. auto. apply Nat.mul_le_mono_nonneg. apply Nat.le_0_l. assumption. apply Nat.le_0_l. apply le_n_S. assumption. Qed. @@ -558,7 +558,7 @@ Proof. remember (S n + p)%nat as n0. assert (n <= n0)%nat. subst n0. simpl. apply le_S. rewrite <- (Nat.add_0_r n). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. - apply Nat.add_le_mono. assumption. apply Nat.div_le_mono. auto. + apply Nat.add_le_mono. assumption. apply Nat.Div0.div_le_mono. auto. apply Nat.mul_le_mono. assumption. apply le_n_S. assumption. rewrite CRabs_minus_sym. apply H. apply Nat.le_refl. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity.