Theorem: Int.nonNeg_mk (Extra/Int/Lemmas.lean)

State before:
case zero_zero

⊢ (0 ⊖ 0).NonNeg ↔ 0 ≤ 0
Tactic:
rw [zero_mk_zero]
State after:
case zero_zero

⊢ NonNeg 0 ↔ 0 ≤ 0

State before:
case zero_zero

⊢ NonNeg 0 ↔ 0 ≤ 0
Tactic:
constructor
State after:
case zero_zero.mp

⊢ NonNeg 0 → 0 ≤ 0

case zero_zero.mpr

⊢ 0 ≤ 0 → NonNeg 0

State before:
case zero_zero.mp

⊢ NonNeg 0 → 0 ≤ 0
Tactic:
intro
State after:
case zero_zero.mp
a✝ : NonNeg 0
⊢ 0 ≤ 0

State before:
case zero_zero.mp
a✝ : NonNeg 0
⊢ 0 ≤ 0
Tactic:
exact Nat.le_refl ..
State after:
no goals

State before:
case zero_zero.mpr

⊢ 0 ≤ 0 → NonNeg 0
Tactic:
intro
State after:
case zero_zero.mpr
a✝ : 0 ≤ 0
⊢ NonNeg 0

State before:
case zero_zero.mpr
a✝ : 0 ≤ 0
⊢ NonNeg 0
Tactic:
apply NonNeg.mk
State after:
no goals

State before:
case zero_succ
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ (0 ⊖ n + 1).NonNeg ↔ n + 1 ≤ 0
Tactic:
rw [zero_mk_succ]
State after:
case zero_succ
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ -[n+1].NonNeg ↔ n + 1 ≤ 0

State before:
case zero_succ
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ -[n+1].NonNeg ↔ n + 1 ≤ 0
Tactic:
constructor
State after:
case zero_succ.mp
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ -[n+1].NonNeg → n + 1 ≤ 0

case zero_succ.mpr
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ n + 1 ≤ 0 → -[n+1].NonNeg

State before:
case zero_succ.mp
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ -[n+1].NonNeg → n + 1 ≤ 0
Tactic:
intro
State after:
case zero_succ.mp
n : Nat
a✝¹ : (0 ⊖ n).NonNeg ↔ n ≤ 0
a✝ : -[n+1].NonNeg
⊢ n + 1 ≤ 0

State before:
case zero_succ.mp
n : Nat
a✝¹ : (0 ⊖ n).NonNeg ↔ n ≤ 0
a✝ : -[n+1].NonNeg
⊢ n + 1 ≤ 0
Tactic:
contradiction
State after:
no goals

State before:
case zero_succ.mpr
n : Nat
a✝ : (0 ⊖ n).NonNeg ↔ n ≤ 0
⊢ n + 1 ≤ 0 → -[n+1].NonNeg
Tactic:
intro
State after:
case zero_succ.mpr
n : Nat
a✝¹ : (0 ⊖ n).NonNeg ↔ n ≤ 0
a✝ : n + 1 ≤ 0
⊢ -[n+1].NonNeg

State before:
case zero_succ.mpr
n : Nat
a✝¹ : (0 ⊖ n).NonNeg ↔ n ≤ 0
a✝ : n + 1 ≤ 0
⊢ -[n+1].NonNeg
Tactic:
contradiction
State after:
no goals

State before:
case succ_zero
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ (m + 1 ⊖ 0).NonNeg ↔ 0 ≤ m + 1
Tactic:
rw [succ_mk_zero]
State after:
case succ_zero
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ (ofNat (m + 1)).NonNeg ↔ 0 ≤ m + 1

State before:
case succ_zero
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ (ofNat (m + 1)).NonNeg ↔ 0 ≤ m + 1
Tactic:
constructor
State after:
case succ_zero.mp
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ (ofNat (m + 1)).NonNeg → 0 ≤ m + 1

case succ_zero.mpr
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ 0 ≤ m + 1 → (ofNat (m + 1)).NonNeg

State before:
case succ_zero.mp
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ (ofNat (m + 1)).NonNeg → 0 ≤ m + 1
Tactic:
intro
State after:
case succ_zero.mp
m : Nat
a✝¹ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
a✝ : (ofNat (m + 1)).NonNeg
⊢ 0 ≤ m + 1

State before:
case succ_zero.mp
m : Nat
a✝¹ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
a✝ : (ofNat (m + 1)).NonNeg
⊢ 0 ≤ m + 1
Tactic:
apply Nat.zero_le
State after:
no goals

State before:
case succ_zero.mpr
m : Nat
a✝ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
⊢ 0 ≤ m + 1 → (ofNat (m + 1)).NonNeg
Tactic:
intro
State after:
case succ_zero.mpr
m : Nat
a✝¹ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
a✝ : 0 ≤ m + 1
⊢ (ofNat (m + 1)).NonNeg

State before:
case succ_zero.mpr
m : Nat
a✝¹ : (m ⊖ 0).NonNeg ↔ 0 ≤ m
a✝ : 0 ≤ m + 1
⊢ (ofNat (m + 1)).NonNeg
Tactic:
apply NonNeg.mk
State after:
no goals

State before:
case succ_succ
m n : Nat
ih : (m ⊖ n).NonNeg ↔ n ≤ m
⊢ (m + 1 ⊖ n + 1).NonNeg ↔ n + 1 ≤ m + 1
Tactic:
rw [succ_mk_succ]
State after:
case succ_succ
m n : Nat
ih : (m ⊖ n).NonNeg ↔ n ≤ m
⊢ (m ⊖ n).NonNeg ↔ n + 1 ≤ m + 1

State before:
case succ_succ
m n : Nat
ih : (m ⊖ n).NonNeg ↔ n ≤ m
⊢ (m ⊖ n).NonNeg ↔ n + 1 ≤ m + 1
Tactic:
rw [Nat.succ_le_succ_iff]
State after:
case succ_succ
m n : Nat
ih : (m ⊖ n).NonNeg ↔ n ≤ m
⊢ (m ⊖ n).NonNeg ↔ n ≤ m

State before:
case succ_succ
m n : Nat
ih : (m ⊖ n).NonNeg ↔ n ≤ m
⊢ (m ⊖ n).NonNeg ↔ n ≤ m
Tactic:
exact ih
State after:
no goals