[ re #1334 ] Some proofs in Data.Nat.Properties (#1411)

Author: gallais

CHANGELOG.md

@@ -91,6 +91,15 @@ Other minor additions
 
 * Added new proofs to `Data.Nat.Properties`:
   ```agda
+  >⇒≢ : _>_ ⇒ _≢_
+
+  pred[n]≤n : pred n ≤ n
+
+  n<1⇒n≡0 : n < 1 → n ≡ 0
+  m<n⇒0<n : m < n → 0 < n
+
+  m≤n*m : 0 < n → m ≤ n * m
+
   ⊔-⊓-absorptive            : Absorptive _⊓_ _
 
   ⊔-⊓-isLattice             : IsLattice _⊔_ _⊓_
@@ -166,3 +175,8 @@ Other minor additions
   *-inverseˡ : ∀ p → 1/ p * p ≡ 1ℚ
   *-inverseʳ : ∀ p → p * 1/ p ≡ 1ℚ
   ```
+
+* Added new proof to `Data.List.Relation.Unary.All.Properties`:
+  ```agda
+  all-upTo : All (_< n) (upTo n)
+  ```

src/Data/List/Relation/Unary/All/Properties.agda

@@ -440,6 +440,12 @@ applyUpTo⁻ f (suc n) (px ∷ _)   (s≤s z≤n)       = px
 applyUpTo⁻ f (suc n) (_  ∷ pxs) (s≤s (s≤s i<n)) =
   applyUpTo⁻ (f ∘ suc) n pxs (s≤s i<n)
 
+------------------------------------------------------------------------
+-- upTo
+
+all-upTo : ∀ n → All (_< n) (upTo n)
+all-upTo n = applyUpTo⁺₁ id n id
+
 ------------------------------------------------------------------------
 -- applyDownFrom
 

src/Data/Nat/Properties.agda

@@ -257,6 +257,9 @@ n≤0⇒n≡0 z≤n = refl
 <⇒≢ : _<_ ⇒ _≢_
 <⇒≢ m<n refl = 1+n≰n m<n
 
+>⇒≢ : _>_ ⇒ _≢_
+>⇒≢ = ≢-sym ∘ <⇒≢
+
 ≤⇒≯ : _≤_ ⇒ _≯_
 ≤⇒≯ (s≤s m≤n) (s≤s n≤m) = ≤⇒≯ m≤n n≤m
 
@@ -389,10 +392,16 @@ n≮n n = <-irrefl (refl {x = n})
 n<1+n : ∀ n → n < suc n
 n<1+n n = ≤-refl
 
+n<1⇒n≡0 : ∀ {n} → n < 1 → n ≡ 0
+n<1⇒n≡0 (s≤s n≤0) = n≤0⇒n≡0 n≤0
+
 n≢0⇒n>0 : ∀ {n} → n ≢ 0 → n > 0
 n≢0⇒n>0 {zero}  0≢0 =  contradiction refl 0≢0
 n≢0⇒n>0 {suc n} _   =  0<1+n
 
+m<n⇒0<n : ∀ {m n} → m < n → 0 < n
+m<n⇒0<n = ≤-trans 0<1+n
+
 m<n⇒n≢0 : ∀ {m n} → m < n → n ≢ 0
 m<n⇒n≢0 (s≤s m≤n) ()
 
@@ -913,6 +922,12 @@ m≤m*n m {n} 0<n = begin
   m * 1 ≤⟨ *-monoʳ-≤ m 0<n ⟩
   m * n ∎
 
+m≤n*m : ∀ m {n} → 0 < n → m ≤ n * m
+m≤n*m m {n} 0<n = begin
+  m     ≤⟨ m≤m*n m 0<n ⟩
+  m * n ≡⟨ *-comm m n ⟩
+  n * m ∎
+
 m<m*n :  ∀ {m n} → 0 < m → 1 < n → m < m * n
 m<m*n {m@(suc m-1)} {n@(suc (suc n-2))} (s≤s _) (s≤s (s≤s _)) = begin-strict
   m           <⟨ s≤s (s≤s (m≤n+m m-1 n-2)) ⟩
@@ -1553,6 +1568,10 @@ m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n
 pred-mono : pred Preserves _≤_ ⟶ _≤_
 pred-mono m≤n = ∸-mono m≤n (≤-refl {1})
 
+pred[n]≤n : ∀ {n} → pred n ≤ n
+pred[n]≤n {zero}  = z≤n
+pred[n]≤n {suc n} = n≤1+n n
+
 ≤pred⇒≤ : ∀ {m n} → m ≤ pred n → m ≤ n
 ≤pred⇒≤ {m} {zero}  le = le
 ≤pred⇒≤ {m} {suc n} le = ≤-step le