'Deprecate Nat.div_le_mono for Div0.div_le_mono'

anandadalton · May 20, 2023 · 09f7719 · 09f7719
1 parent 4fccdc0
commit 09f7719
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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.