Proof of n≤1⇒n≡0∨n≡1 (#1771)

Author: Akshobhya1234

CHANGELOG.md

@@ -1306,6 +1306,8 @@ Other minor changes
 
   anyUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n)
   allUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n)
+
+  n≤1⇒n≡0∨n≡1 : ∀ {n : ℕ} → n ≤ 1 → n ≡ 0 ⊎ n ≡ 1
   ```
 
 * Added new functions in `Data.Nat`:

src/Data/Nat/Properties.agda

@@ -268,6 +268,10 @@ n≤1+n _ = ≤-step ≤-refl
 n≤0⇒n≡0 : ∀ {n} → n ≤ 0 → n ≡ 0
 n≤0⇒n≡0 z≤n = refl
 
+n≤1⇒n≡0∨n≡1 : ∀ {n : ℕ} → n ≤ 1 → n ≡ 0 ⊎ n ≡ 1
+n≤1⇒n≡0∨n≡1 z≤n       = inj₁ refl
+n≤1⇒n≡0∨n≡1 (s≤s z≤n) = inj₂ refl
+
 ------------------------------------------------------------------------
 -- Properties of _<_
 ------------------------------------------------------------------------