m n k : Nat
h : m < n ∨ m ≥ n
⊢ subNatNat m n + -[k+1] = subNatNat m (n + succ k)
m n k : Nat
⊢ subNatNat m n + -[k+1] = subNatNat m (n + succ k)
have h := Nat.lt_or_ge m n
no goals
m n k : Nat
h : m < n ∨ m ≥ n
⊢ subNatNat m n + -[k+1] = subNatNat m (n + succ k)
cases h with
| inr h' =>
  rw [subNatNat_of_le h']
  simp
  rw [subNatNat_sub h', Nat.add_comm]
| inl h' =>
  have h₂ : m < n + succ k := Nat.lt_of_lt_of_le h' (le_add_right _ _)
  have h₃ : m ≤ n + k := le_of_succ_le_succ h₂
  rw [subNatNat_of_lt h', subNatNat_of_lt h₂]
  simp [Nat.add_comm]
  rw [← add_succ, succ_pred_eq_of_pos (Nat.sub_pos_of_lt h'), add_succ, succ_sub h₃, Nat.pred_succ]
  rw [Nat.add_comm n, Nat.add_sub_assoc (Nat.le_of_lt h')]
case inr
m n k : Nat
h' : m ≥ n
⊢ ↑(m - n) + -[k+1] = subNatNat m (n + succ k)
case inr
m n k : Nat
h' : m ≥ n
⊢ subNatNat m n + -[k+1] = subNatNat m (n + succ k)
rw [subNatNat_of_le h']
case inr
m n k : Nat
h' : m ≥ n
⊢ subNatNat (m - n) (succ k) = subNatNat m (n + succ k)
case inr
m n k : Nat
h' : m ≥ n
⊢ ↑(m - n) + -[k+1] = subNatNat m (n + succ k)
simp
no goals
case inr
m n k : Nat
h' : m ≥ n
⊢ subNatNat (m - n) (succ k) = subNatNat m (n + succ k)
rw [subNatNat_sub h', Nat.add_comm]
case inl
m n k : Nat
h' : m < n
h₂ : m < n + succ k
⊢ subNatNat m n + -[k+1] = subNatNat m (n + succ k)
case inl
m n k : Nat
h' : m < n
⊢ subNatNat m n + -[k+1] = subNatNat m (n + succ k)
have h₂ : m < n + succ k := Nat.lt_of_lt_of_le h' (le_add_right _ _)
case inl
m n k : Nat
h' : m < n
h₂ : m < n + succ k
h₃ : m ≤ n + k
⊢ subNatNat m n + -[k+1] = subNatNat m (n + succ k)
case inl
m n k : Nat
h' : m < n
h₂ : m < n + succ k
⊢ subNatNat m n + -[k+1] = subNatNat m (n + succ k)
have h₃ : m ≤ n + k := le_of_succ_le_succ h₂
case inl
m n k : Nat
h' : m < n
h₂ : m < n + succ k
h₃ : m ≤ n + k
⊢ -[pred (n - m)+1] + -[k+1] = -[pred (n + succ k - m)+1]
case inl
m n k : Nat
h' : m < n
h₂ : m < n + succ k
h₃ : m ≤ n + k
⊢ subNatNat m n + -[k+1] = subNatNat m (n + succ k)
rw [subNatNat_of_lt h', subNatNat_of_lt h₂]
case inl
m n k : Nat
h' : m < n
h₂ : m < n + succ k
h₃ : m ≤ n + k
⊢ succ (k + pred (n - m)) = pred (n + succ k - m)
case inl
m n k : Nat
h' : m < n
h₂ : m < n + succ k
h₃ : m ≤ n + k
⊢ -[pred (n - m)+1] + -[k+1] = -[pred (n + succ k - m)+1]
simp [Nat.add_comm]
case inl
m n k : Nat
h' : m < n
h₂ : m < n + succ k
h₃ : m ≤ n + k
⊢ k + (n - m) = n + k - m
case inl
m n k : Nat
h' : m < n
h₂ : m < n + succ k
h₃ : m ≤ n + k
⊢ succ (k + pred (n - m)) = pred (n + succ k - m)
rw [← add_succ, succ_pred_eq_of_pos (Nat.sub_pos_of_lt h'), add_succ, succ_sub h₃, Nat.pred_succ]
no goals
case inl
m n k : Nat
h' : m < n
h₂ : m < n + succ k
h₃ : m ≤ n + k
⊢ k + (n - m) = n + k - m
rw [Nat.add_comm n, Nat.add_sub_assoc (Nat.le_of_lt h')]