{ intro himp
  apply True.intro }
case mp
m n : ℕ
p : Prop
hge : m ≥ n
⊢ (m < n → p) → True

case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p