Theorem: s₃ (Fl.lean)

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d
Tactic:
have hfc : round (a - round (a - b)) = a - round (a - b) := by
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
State after:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d
Tactic:
have helo : round (a - b) = trunc n (a - b) := by
  apply round_eq_trunc_of_le npos hfaithful₁
  apply Nat.le_of_lt
  rewrite [lt_tsub_comm, ← hfc]
  exact hbc
State after:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d
Tactic:
have hcd : round (a - round (a - b)) ≤ 2 * d := by
  trans 2 * b
  . rewrite [hfc, helo]
    exact s₃' npos hfa hab
  . exact Nat.mul_le_mul_left 2 hbd
State after:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
hcd : round (a - round (a - b)) ≤ 2 * d
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
hcd : round (a - round (a - b)) ≤ 2 * d
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d
Tactic:
have hfe : trunc n (round (a - round (a - b))) = round (a - round (a - b)) :=
  trunc_round npos hfaithful₁ (a - round (a - b))
State after:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
hcd : round (a - round (a - b)) ≤ 2 * d
hfe : trunc n (round (a - round (a - b))) = round (a - round (a - b))
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
hcd : round (a - round (a - b)) ≤ 2 * d
hfe : trunc n (round (a - round (a - b))) = round (a - round (a - b))
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d
Tactic:
exact sterbenz hfe hfd hdc hcd
State after:
no goals

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
⊢ round (a - round (a - b)) = a - round (a - b)
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
State after:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
⊢ trunc n (a - round (a - b)) = a - round (a - b)

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
State after:
no goals

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) = trunc n (a - b)
Tactic:
apply round_eq_trunc_of_le npos hfaithful₁
State after:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) ≤ a - b

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) ≤ a - b
Tactic:
apply Nat.le_of_lt
State after:
case h
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) < a - b

State before:
case h
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) < a - b
Tactic:
rewrite [lt_tsub_comm, ← hfc]
State after:
case h
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
⊢ b < round (a - round (a - b))

State before:
case h
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
⊢ b < round (a - round (a - b))
Tactic:
exact hbc
State after:
no goals

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ round (a - round (a - b)) ≤ 2 * d
Tactic:
trans 2 * b
State after:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ round (a - round (a - b)) ≤ 2 * b

d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ 2 * b ≤ 2 * d

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ round (a - round (a - b)) ≤ 2 * b

d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ 2 * b ≤ 2 * d
Tactic:
. rewrite [hfc, helo]
  exact s₃' npos hfa hab
State after:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ 2 * b ≤ 2 * d

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ 2 * b ≤ 2 * d
Tactic:
. exact Nat.mul_le_mul_left 2 hbd
State after:
no goals

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ round (a - round (a - b)) ≤ 2 * b
Tactic:
rewrite [hfc, helo]
State after:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ a - trunc n (a - b) ≤ 2 * b

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ a - trunc n (a - b) ≤ 2 * b
Tactic:
exact s₃' npos hfa hab
State after:
no goals

State before:
d : ℕ
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
helo : round (a - b) = trunc n (a - b)
⊢ 2 * b ≤ 2 * d
Tactic:
exact Nat.mul_le_mul_left 2 hbd
State after:
no goals