Theorem: trunc_le_size_sub_ulp (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a ≤ 2 ^ Nat.size a - ulp n a
Tactic:
rewrite [← size_trunc_eq_size npos]
State after:
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a ≤ 2 ^ Nat.size (trunc n a) - ulp n a

State before:
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a ≤ 2 ^ Nat.size (trunc n a) - ulp n a
Tactic:
rewrite [← ulp_trunc npos]
State after:
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a ≤ 2 ^ Nat.size (trunc n a) - ulp n (trunc n a)

State before:
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a ≤ 2 ^ Nat.size (trunc n a) - ulp n (trunc n a)
Tactic:
apply le_sub_of_dvd_of_dvd_of_lt
State after:
case h₁
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ trunc n a

case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)

case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)

State before:
case h₁
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ trunc n a

case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)

case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Tactic:
. exact ulp_dvd_of_trunc_eq (trunc_idempotent npos _)
State after:
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)

case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)

State before:
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)

case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Tactic:
. rewrite [ulp, expt, Nat.pow_dvd_pow_iff_le_right one_lt_two]
  exact tsub_le_self
State after:
case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)

State before:
case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Tactic:
. exact Nat.lt_size_self _
State after:
no goals

State before:
case h₁
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ trunc n a
Tactic:
exact ulp_dvd_of_trunc_eq (trunc_idempotent npos _)
State after:
no goals

State before:
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ ulp n (trunc n a) ∣ 2 ^ Nat.size (trunc n a)
Tactic:
rewrite [ulp, expt, Nat.pow_dvd_pow_iff_le_right one_lt_two]
State after:
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ Nat.size (trunc n a) - n ≤ Nat.size (trunc n a)

State before:
case h₂
n : ℕ
npos : 0 < n
a : ℕ
⊢ Nat.size (trunc n a) - n ≤ Nat.size (trunc n a)
Tactic:
exact tsub_le_self
State after:
no goals

State before:
case h₃
n : ℕ
npos : 0 < n
a : ℕ
⊢ trunc n a < 2 ^ Nat.size (trunc n a)
Tactic:
exact Nat.lt_size_self _
State after:
no goals