widen.agda

data bool : Set where
  tt : bool
  ff : bool

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
succ m + n = succ (m + n)

_<_ : ℕ → ℕ → bool
m < zero = ff
zero < succ n = tt
succ m < succ n = m < n

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

widen : ∀ m n p → (m < n) ≡ tt → (m < (n + p)) ≡ tt
widen m zero p ()
widen zero (succ n) p refl = refl
widen (succ m) (succ n) p e = widen m n p e