diff --git a/CHANGELOG.md b/CHANGELOG.md index a58227662c..2f5b9ff7da 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -322,6 +322,11 @@ Additions to existing modules ```agda m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o m≤n⇒m≤o*n : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ o * n + <‴-irrefl : Irreflexive _≡_ _<‴_ + ≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_ + <‴-irrelevant : Irrelevant {A = ℕ} _<‴_ + >‴-irrelevant : Irrelevant {A = ℕ} _>‴_ + ≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_ ``` adjunction between `suc` and `pred` diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index b7a7c00511..68efe6bcdf 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -2237,6 +2237,27 @@ _>‴?_ = flip _<‴?_ ≤‴⇒≤ : _≤‴_ ⇒ _≤_ ≤‴⇒≤ = ≤″⇒≤ ∘ ≤‴⇒≤″ +<‴-irrefl : Irreflexive _≡_ _<‴_ +<‴-irrefl eq = <-irrefl eq ∘ ≤‴⇒≤ + +≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_ +≤‴-irrelevant ≤‴-refl = lemma refl + where + lemma : ∀ {m n} → (e : m ≡ n) → (q : m ≤‴ n) → subst (m ≤‴_) e ≤‴-refl ≡ q + lemma {m} e ≤‴-refl = cong (λ e → subst (m ≤‴_) e ≤‴-refl) $ ≡-irrelevant e refl + lemma refl (≤‴-step m‴-irrelevant : Irrelevant {A = ℕ} _>‴_ +>‴-irrelevant = ≤‴-irrelevant + +≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_ +≥‴-irrelevant = ≤‴-irrelevant + ------------------------------------------------------------------------ -- Other properties ------------------------------------------------------------------------