Theorem: s₁ (Fl.lean)

State before:
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
⊢ trunc n (c - a) = c - a
Tactic:
cases le_or_gt c (2 * a) with
| inl hle => exact sterbenz hfc hfa hac hle
| inr hgt =>
  rewrite [← hfc]
  rewrite [← tsub_tsub_cancel_of_le hcb]
  apply s₁' npos hfb hf
  rewrite [tsub_tsub_cancel_of_le hcb]
  exact hgt
State after:
no goals

State before:
case inl
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hle : c ≤ 2 * a
⊢ trunc n (c - a) = c - a
Tactic:
exact sterbenz hfc hfa hac hle
State after:
no goals

State before:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ trunc n (c - a) = c - a
Tactic:
rewrite [← hfc]
State after:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ trunc n (trunc n c - a) = trunc n c - a

State before:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ trunc n (trunc n c - a) = trunc n c - a
Tactic:
rewrite [← tsub_tsub_cancel_of_le hcb]
State after:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ trunc n (trunc n (b - (b - c)) - a) = trunc n (b - (b - c)) - a

State before:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ trunc n (trunc n (b - (b - c)) - a) = trunc n (b - (b - c)) - a
Tactic:
apply s₁' npos hfb hf
State after:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ 2 * a < b - (b - c)

State before:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ 2 * a < b - (b - c)
Tactic:
rewrite [tsub_tsub_cancel_of_le hcb]
State after:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ 2 * a < c

State before:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ 2 * a < c
Tactic:
exact hgt
State after:
no goals