dsfsdf.agda

module ≤-Reasoning where
  open import plfa.part1.Relations using (_≤_;≤-trans;s≤s;z≤n;≤-refl)
  open import Data.Nat hiding (_≤_)
  open import Data.Nat.Properties using (+-comm;+-suc)
  
  infix  1 begin_
  infixr 2 _≤⟨⟩_ _≤⟨_⟩_
  infix  3 _∎

  begin_ : ∀ {x y : ℕ}
         → x ≤ y
         → x ≤ y
  begin x≤y = x≤y

  _≤⟨⟩_ : ∀ (x : ℕ) {y : ℕ}
        → x ≤ y
        → x ≤ y
  x ≤⟨⟩ x≤y = x≤y

  _≤⟨_⟩_ : ∀ (x : ℕ) {y z : ℕ}
         → x ≤ y
         → y ≤ z
         → x ≤ z
  x ≤⟨ x≤y ⟩ y≤z = ≤-trans x≤y y≤z

  _∎ : ∀ (x : ℕ) → x ≤ x
  x ∎ = ≤-refl

  -- (c)lean
  +-monoʳ-≤c : ∀ (n p q : ℕ) → p ≤ q → n + p ≤ n + q
  +-monoʳ-≤c zero p q p≤q = p≤q
  +-monoʳ-≤c (suc n) p q p≤q = s≤s (+-monoʳ-≤c n p q p≤q)
  
  -- What are these nats even conveying to the reader?
  +-monoʳ-≤ : ∀ (n p q : ℕ) → p ≤ q → n + p ≤ n + q
  +-monoʳ-≤ zero p q p≤q = p≤q
  +-monoʳ-≤ (suc n) p q p≤q =
    begin
      suc n + p -- ???
    ≤⟨ s≤s (+-monoʳ-≤ n p q p≤q) ⟩
      suc (n + q) -- ???
    ∎