Theorem: s₁' (Fl.lean)

State before:
n a b x : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - x
⊢ trunc n (trunc n (b - x) - a) = trunc n (b - x) - a
Tactic:
induction x with
| zero =>
  rewrite [Nat.sub_zero]
  rewrite [hfb]
  exact hf
| succ w ih =>
  replace ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a := by
    apply ih
    apply Nat.lt_of_lt_of_le h
    apply tsub_le_tsub_left
    exact Nat.le_succ w
  rewrite [Nat.sub_succ, Nat.pred_eq_sub_one]
  cases eq_or_ne (trunc n (b - w)) (b - w) with
  | inr ne =>
    rewrite [trunc_pred_eq_trunc_of_trunc_ne_self npos ne]
    exact ih
  | inl hfb₁ =>
    have bpos : 0 < b - w :=
      Nat.zero_lt_of_lt $ Nat.lt_pred_iff.mp $ Nat.sub_succ _ _ ▸ h
    rewrite [trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq bpos hfb₁]
    rewrite [tsub_right_comm]
    rewrite [trunc_eq_iff_ulp_dvd]
    apply Nat.dvd_sub'
    . calc ulp n (b - w - a - ulp n (b - w - 1))
        _ ∣ ulp n (b - w - a) := ulp_dvd_ulp n tsub_le_self
        _ ∣ b - w - a         := ulp_dvd_of_trunc_eq $ hfb₁ ▸ ih
    . apply ulp_dvd_ulp
      calc b - w - a - ulp n (b - w - 1)
        _ ≤ b - w - a - 1 := tsub_le_tsub_left (Nat.one_le_of_lt $ ulp_pos n _) _
        _ ≤ b - w - 1     := tsub_le_tsub_right tsub_le_self _
State after:
no goals

State before:
case zero
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - Nat.zero
⊢ trunc n (trunc n (b - Nat.zero) - a) = trunc n (b - Nat.zero) - a
Tactic:
rewrite [Nat.sub_zero]
State after:
case zero
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - Nat.zero
⊢ trunc n (trunc n b - a) = trunc n b - a

State before:
case zero
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - Nat.zero
⊢ trunc n (trunc n b - a) = trunc n b - a
Tactic:
rewrite [hfb]
State after:
case zero
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - Nat.zero
⊢ trunc n (b - a) = b - a

State before:
case zero
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - Nat.zero
⊢ trunc n (b - a) = b - a
Tactic:
exact hf
State after:
no goals

State before:
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ trunc n (trunc n (b - Nat.succ w) - a) = trunc n (b - Nat.succ w) - a
Tactic:
replace ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a := by
  apply ih
  apply Nat.lt_of_lt_of_le h
  apply tsub_le_tsub_left
  exact Nat.le_succ w
State after:
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
⊢ trunc n (trunc n (b - Nat.succ w) - a) = trunc n (b - Nat.succ w) - a

State before:
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
⊢ trunc n (trunc n (b - Nat.succ w) - a) = trunc n (b - Nat.succ w) - a
Tactic:
rewrite [Nat.sub_succ, Nat.pred_eq_sub_one]
State after:
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a

State before:
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
Tactic:
cases eq_or_ne (trunc n (b - w)) (b - w) with
| inr ne =>
  rewrite [trunc_pred_eq_trunc_of_trunc_ne_self npos ne]
  exact ih
| inl hfb₁ =>
  have bpos : 0 < b - w :=
    Nat.zero_lt_of_lt $ Nat.lt_pred_iff.mp $ Nat.sub_succ _ _ ▸ h
  rewrite [trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq bpos hfb₁]
  rewrite [tsub_right_comm]
  rewrite [trunc_eq_iff_ulp_dvd]
  apply Nat.dvd_sub'
  . calc ulp n (b - w - a - ulp n (b - w - 1))
      _ ∣ ulp n (b - w - a) := ulp_dvd_ulp n tsub_le_self
      _ ∣ b - w - a         := ulp_dvd_of_trunc_eq $ hfb₁ ▸ ih
  . apply ulp_dvd_ulp
    calc b - w - a - ulp n (b - w - 1)
      _ ≤ b - w - a - 1 := tsub_le_tsub_left (Nat.one_le_of_lt $ ulp_pos n _) _
      _ ≤ b - w - 1     := tsub_le_tsub_right tsub_le_self _
State after:
no goals

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
Tactic:
apply ih
State after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ 2 * a < b - w

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ 2 * a < b - w
Tactic:
apply Nat.lt_of_lt_of_le h
State after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ b - Nat.succ w ≤ b - w

State before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ b - Nat.succ w ≤ b - w
Tactic:
apply tsub_le_tsub_left
State after:
case h
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ w ≤ Nat.succ w

State before:
case h
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ w ≤ Nat.succ w
Tactic:
exact Nat.le_succ w
State after:
no goals

State before:
case succ.inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
ne : trunc n (b - w) ≠ b - w
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
Tactic:
rewrite [trunc_pred_eq_trunc_of_trunc_ne_self npos ne]
State after:
case succ.inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
ne : trunc n (b - w) ≠ b - w
⊢ trunc n (trunc n (b - w) - a) = trunc n (b - w) - a

State before:
case succ.inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
ne : trunc n (b - w) ≠ b - w
⊢ trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
Tactic:
exact ih
State after:
no goals

State before:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
Tactic:
have bpos : 0 < b - w :=
  Nat.zero_lt_of_lt $ Nat.lt_pred_iff.mp $ Nat.sub_succ _ _ ▸ h
State after:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a

State before:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
Tactic:
rewrite [trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq bpos hfb₁]
State after:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (b - w - ulp n (b - w - 1) - a) = b - w - ulp n (b - w - 1) - a

State before:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (b - w - ulp n (b - w - 1) - a) = b - w - ulp n (b - w - 1) - a
Tactic:
rewrite [tsub_right_comm]
State after:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (b - w - a - ulp n (b - w - 1)) = b - w - a - ulp n (b - w - 1)

State before:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (b - w - a - ulp n (b - w - 1)) = b - w - a - ulp n (b - w - 1)
Tactic:
rewrite [trunc_eq_iff_ulp_dvd]
State after:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ b - w - a - ulp n (b - w - 1)

State before:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ b - w - a - ulp n (b - w - 1)
Tactic:
apply Nat.dvd_sub'
State after:
case succ.inl.h₁
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ b - w - a

case succ.inl.h₂
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ ulp n (b - w - 1)

State before:
case succ.inl.h₁
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ b - w - a

case succ.inl.h₂
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ ulp n (b - w - 1)
Tactic:
. calc ulp n (b - w - a - ulp n (b - w - 1))
    _ ∣ ulp n (b - w - a) := ulp_dvd_ulp n tsub_le_self
    _ ∣ b - w - a         := ulp_dvd_of_trunc_eq $ hfb₁ ▸ ih
State after:
case succ.inl.h₂
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ ulp n (b - w - 1)

State before:
case succ.inl.h₂
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ ulp n (b - w - 1)
Tactic:
. apply ulp_dvd_ulp
  calc b - w - a - ulp n (b - w - 1)
    _ ≤ b - w - a - 1 := tsub_le_tsub_left (Nat.one_le_of_lt $ ulp_pos n _) _
    _ ≤ b - w - 1     := tsub_le_tsub_right tsub_le_self _
State after:
no goals

State before:
case succ.inl.h₁
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ b - w - a
Tactic:
calc ulp n (b - w - a - ulp n (b - w - 1))
  _ ∣ ulp n (b - w - a) := ulp_dvd_ulp n tsub_le_self
  _ ∣ b - w - a         := ulp_dvd_of_trunc_eq $ hfb₁ ▸ ih
State after:
no goals

State before:
case succ.inl.h₂
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ ulp n (b - w - 1)
Tactic:
apply ulp_dvd_ulp
State after:
case succ.inl.h₂.h
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ b - w - a - ulp n (b - w - 1) ≤ b - w - 1

State before:
case succ.inl.h₂.h
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ b - w - a - ulp n (b - w - 1) ≤ b - w - 1
Tactic:
calc b - w - a - ulp n (b - w - 1)
  _ ≤ b - w - a - 1 := tsub_le_tsub_left (Nat.one_le_of_lt $ ulp_pos n _) _
  _ ≤ b - w - 1     := tsub_le_tsub_right tsub_le_self _
State after:
no goals