Theorem: MyNat.lt_iff_succ_le (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
⊢ a < b ↔ succ a ≤ b
Tactic:
constructor
State after:
case mp
a b : Nat
⊢ a < b → succ a ≤ b

case mpr
a b : Nat
⊢ succ a ≤ b → a < b

State before:
a b : Nat
⊢ a < b → succ a ≤ b
Tactic:
case mp => exact lt_aux_one _ _
State after:
no goals

State before:
a b : Nat
⊢ succ a ≤ b → a < b
Tactic:
case mpr => exact lt_aux_two _ _
State after:
no goals

State before:
a b : Nat
⊢ a < b → succ a ≤ b
Tactic:
exact lt_aux_one _ _
State after:
no goals

State before:
a b : Nat
⊢ succ a ≤ b → a < b
Tactic:
exact lt_aux_two _ _
State after:
no goals