Theorem: next_trunc_of_carry (Fl/Trunc.lean)

State before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n (trunc n x) = 2 ^ Nat.size x
Tactic:
unfold next
State after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n x + ulp n (trunc n x) = 2 ^ Nat.size x

State before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n x + ulp n (trunc n x) = 2 ^ Nat.size x
Tactic:
rewrite [ulp_trunc npos]
State after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n x + ulp n x = 2 ^ Nat.size x

State before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n x + ulp n x = 2 ^ Nat.size x
Tactic:
unfold trunc ulp
State after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x / 2 ^ expt n x * 2 ^ expt n x + 2 ^ expt n x = 2 ^ Nat.size x

State before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x / 2 ^ expt n x * 2 ^ expt n x + 2 ^ expt n x = 2 ^ Nat.size x
Tactic:
rewrite [← Nat.succ_mul]
State after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.succ (x / 2 ^ expt n x) * 2 ^ expt n x = 2 ^ Nat.size x

State before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.succ (x / 2 ^ expt n x) * 2 ^ expt n x = 2 ^ Nat.size x
Tactic:
rewrite [← Nat.add_div_right x two_pow_pos]
State after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x

State before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x
Tactic:
have h₁ : expt n x ≤ Nat.size x := tsub_le_self
State after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
h₁ : expt n x ≤ Nat.size x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x

State before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
h₁ : expt n x ≤ Nat.size x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x
Tactic:
have h₃ : next n x < 2 ^ Nat.size x + 2 ^ expt n x :=
  Nat.add_lt_add_right (Nat.lt_size_self x) _
State after:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
h₁ : expt n x ≤ Nat.size x
h₃ : next n x < 2 ^ Nat.size x + 2 ^ expt n x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x

State before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
h₁ : expt n x ≤ Nat.size x
h₃ : next n x < 2 ^ Nat.size x + 2 ^ expt n x
⊢ (x + 2 ^ expt n x) / 2 ^ expt n x * 2 ^ expt n x = 2 ^ Nat.size x
Tactic:
exact div_mul_eq_of_le_of_lt h₁ carry h₃
State after:
no goals