Theorem: ENat.mono_add (GMLInit/Data/Nat/Extended/Basic.lean)

State before:
n m : Nat
x : ENat
⊢ x.leNat n = true → x.leNat (n + m) = true
Tactic:
intro h
State after:
n m : Nat
x : ENat
h : x.leNat n = true
⊢ x.leNat (n + m) = true

State before:
n m : Nat
x : ENat
h : x.leNat n = true
⊢ x.leNat (n + m) = true
Tactic:
induction m with
| zero => exact h
| succ _ h => exact mono_step _ h
State after:
no goals

State before:
case zero
n : Nat
x : ENat
h : x.leNat n = true
⊢ x.leNat (n + 0) = true
Tactic:
exact h
State after:
no goals

State before:
case succ
n : Nat
x : ENat
h✝ : x.leNat n = true
n✝ : Nat
h : x.leNat (n + n✝) = true
⊢ x.leNat (n + (n✝ + 1)) = true
Tactic:
exact mono_step _ h
State after:
no goals