a b : Int
⊢ ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Int
⊢ natAbs (a + b) ≤ natAbs a + natAbs b
suffices ∀ a b : Nat, natAbs (subNatNat a b.succ) ≤ (a + b).succ by
  match a, b with
  | (a:Nat), (b:Nat) => simp
  | (a:Nat), -[b+1]  => simp; apply this
  | -[a+1],  (b:Nat) => simp [Nat.succ_add, Nat.add_comm a b]; apply this
  | -[a+1],  -[b+1]  => simp [Nat.succ_add]; apply Nat.le_refl
case refine_1
a✝ b✝ : Int
a b : Nat
⊢ ∀ (i n : Nat), (fun m n i => n = succ b → natAbs i ≤ succ (m + b)) (n + i) n ↑i

case refine_2
a✝ b✝ : Int
a b i n : Nat
e : succ (n + i) = succ b
⊢ natAbs -[i+1] ≤ succ (n + b)
a b : Int
⊢ ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
refine fun a b => subNatNat_elim a b.succ
  (fun m n i => n = b.succ → natAbs i ≤ (m + b).succ) ?_
  (fun i n (e : (n + i).succ = _) => ?_) rfl
no goals
a b : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
⊢ natAbs (a + b) ≤ natAbs a + natAbs b
match a, b with
| (a:Nat), (b:Nat) => simp
| (a:Nat), -[b+1]  => simp; apply this
| -[a+1],  (b:Nat) => simp [Nat.succ_add, Nat.add_comm a b]; apply this
| -[a+1],  -[b+1]  => simp [Nat.succ_add]; apply Nat.le_refl
no goals
a✝ b✝ : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Nat
⊢ natAbs (↑a + ↑b) ≤ natAbs ↑a + natAbs ↑b
simp
a✝ b✝ : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Nat
⊢ natAbs (subNatNat a (succ b)) ≤ a + succ b
a✝ b✝ : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Nat
⊢ natAbs (↑a + -[b+1]) ≤ natAbs ↑a + natAbs -[b+1]
simp
no goals
a✝ b✝ : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Nat
⊢ natAbs (subNatNat a (succ b)) ≤ a + succ b
apply this
a✝ b✝ : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Nat
⊢ natAbs (subNatNat b (succ a)) ≤ succ (b + a)
a✝ b✝ : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Nat
⊢ natAbs (-[a+1] + ↑b) ≤ natAbs -[a+1] + natAbs ↑b
simp [Nat.succ_add, Nat.add_comm a b]
no goals
a✝ b✝ : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Nat
⊢ natAbs (subNatNat b (succ a)) ≤ succ (b + a)
apply this
a✝ b✝ : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Nat
⊢ succ (succ (a + b)) ≤ succ (a + succ b)
a✝ b✝ : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Nat
⊢ natAbs (-[a+1] + -[b+1]) ≤ natAbs -[a+1] + natAbs -[b+1]
simp [Nat.succ_add]
no goals
a✝ b✝ : Int
this : ∀ (a b : Nat), natAbs (subNatNat a (succ b)) ≤ succ (a + b)
a b : Nat
⊢ succ (succ (a + b)) ≤ succ (a + succ b)
apply Nat.le_refl
case refine_1
a✝ b✝ : Int
a b i : Nat
⊢ natAbs ↑i ≤ succ (succ b + i + b)
case refine_1
a✝ b✝ : Int
a b : Nat
⊢ ∀ (i n : Nat), (fun m n i => n = succ b → natAbs i ≤ succ (m + b)) (n + i) n ↑i
rintro i n rfl
case refine_1
a✝ b✝ : Int
a b i : Nat
⊢ natAbs ↑i ≤ succ (i + (succ b + b))
case refine_1
a✝ b✝ : Int
a b i : Nat
⊢ natAbs ↑i ≤ succ (succ b + i + b)
rw [Nat.add_comm _ i, Nat.add_assoc]
no goals
case refine_1
a✝ b✝ : Int
a b i : Nat
⊢ natAbs ↑i ≤ succ (i + (succ b + b))
exact Nat.le_add_right i (b.succ + b).succ
case refine_2.a
a✝ b✝ : Int
a b i n : Nat
e : succ (n + i) = succ b
⊢ i ≤ n + b
case refine_2
a✝ b✝ : Int
a b i n : Nat
e : succ (n + i) = succ b
⊢ natAbs -[i+1] ≤ succ (n + b)
apply succ_le_succ
case refine_2.a
a✝ b✝ : Int
a b i n : Nat
e : succ (n + i) = succ b
⊢ i ≤ i + (n + n)
case refine_2.a
a✝ b✝ : Int
a b i n : Nat
e : succ (n + i) = succ b
⊢ i ≤ n + b
rw [← succ.inj e, ← Nat.add_assoc, Nat.add_comm]
no goals
case refine_2.a
a✝ b✝ : Int
a b i n : Nat
e : succ (n + i) = succ b
⊢ i ≤ i + (n + n)
apply Nat.le_add_right