Theorem: a₁_lo_of_no_carry_of_round_le (Fl.lean)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have size_eq : Nat.size (a + b) = Nat.size a := by
  apply Nat.le_antisymm
  . exact Nat.size_le.mpr no_carry
  . exact Nat.size_le_size (Nat.le_add_right _ _)
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have ulp_eq : ulp n (a + b) = ulp n a := by
  unfold ulp expt
  rw [size_eq]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have mod_ulp₁ : a % ulp n a = 0 := by
  apply Nat.mod_eq_zero_of_dvd
  exact ulp_dvd_of_trunc_eq hfa
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have mod_ulp₂ : (a + b) % ulp n a = b % ulp n a := by
  rw [Nat.add_mod, mod_ulp₁, Nat.zero_add, Nat.mod_mod]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
have error_eq : a + b - trunc n (a + b) = b % ulp n a := by
  rewrite [tsub_eq_iff_eq_add_of_le (trunc_le _ _), Nat.add_comm (b % ulp n a)]
  rewrite [← mod_ulp₂, ← ulp_eq]
  unfold trunc
  rw [Nat.div_add_mod']
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ trunc n (a + b - round (a + b)) = a + b - round (a + b)
Tactic:
rewrite [round_eq_trunc_of_le npos hfaithful₁ round_le, error_eq]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ trunc n (b % ulp n a) = b % ulp n a

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ trunc n (b % ulp n a) = b % ulp n a
Tactic:
apply trunc_eq_of_le_of_ulp_dvd b
State after:
case hle
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ b % ulp n a ≤ b

case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ ulp n b ∣ b % ulp n a

State before:
case hle
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ b % ulp n a ≤ b

case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ ulp n b ∣ b % ulp n a
Tactic:
. exact Nat.mod_le _ _
State after:
case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ ulp n b ∣ b % ulp n a

State before:
case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ ulp n b ∣ b % ulp n a
Tactic:
. rewrite [Nat.dvd_mod_iff (ulp_dvd_ulp n hba)]
  exact ulp_dvd_of_trunc_eq hfb
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size (a + b) = Nat.size a
Tactic:
apply Nat.le_antisymm
State after:
case h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a

case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size a ≤ Nat.size (a + b)

State before:
case h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a

case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
. exact Nat.size_le.mpr no_carry
State after:
case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size a ≤ Nat.size (a + b)

State before:
case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
. exact Nat.size_le_size (Nat.le_add_right _ _)
State after:
no goals

State before:
case h₁
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size (a + b) ≤ Nat.size a
Tactic:
exact Nat.size_le.mpr no_carry
State after:
no goals

State before:
case h₂
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
⊢ Nat.size a ≤ Nat.size (a + b)
Tactic:
exact Nat.size_le_size (Nat.le_add_right _ _)
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
⊢ ulp n (a + b) = ulp n a
Tactic:
unfold ulp expt
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a - n)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
⊢ 2 ^ (Nat.size (a + b) - n) = 2 ^ (Nat.size a - n)
Tactic:
rw [size_eq]
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
⊢ a % ulp n a = 0
Tactic:
apply Nat.mod_eq_zero_of_dvd
State after:
case H
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
⊢ ulp n a ∣ a

State before:
case H
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
⊢ ulp n a ∣ a
Tactic:
exact ulp_dvd_of_trunc_eq hfa
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
⊢ (a + b) % ulp n a = b % ulp n a
Tactic:
rw [Nat.add_mod, mod_ulp₁, Nat.zero_add, Nat.mod_mod]
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
⊢ a + b - trunc n (a + b) = b % ulp n a
Tactic:
rewrite [tsub_eq_iff_eq_add_of_le (trunc_le _ _), Nat.add_comm (b % ulp n a)]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
⊢ a + b = trunc n (a + b) + b % ulp n a

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
⊢ a + b = trunc n (a + b) + b % ulp n a
Tactic:
rewrite [← mod_ulp₂, ← ulp_eq]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
⊢ a + b = trunc n (a + b) + (a + b) % ulp n (a + b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
⊢ a + b = trunc n (a + b) + (a + b) % ulp n (a + b)
Tactic:
unfold trunc
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
⊢ a + b = (a + b) / ulp n (a + b) * ulp n (a + b) + (a + b) % ulp n (a + b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
⊢ a + b = (a + b) / ulp n (a + b) * ulp n (a + b) + (a + b) % ulp n (a + b)
Tactic:
rw [Nat.div_add_mod']
State after:
no goals

State before:
case hle
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ b % ulp n a ≤ b
Tactic:
exact Nat.mod_le _ _
State after:
no goals

State before:
case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ ulp n b ∣ b % ulp n a
Tactic:
rewrite [Nat.dvd_mod_iff (ulp_dvd_ulp n hba)]
State after:
case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ ulp n b ∣ b

State before:
case hdvd
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_carry : a + b < 2 ^ Nat.size a
round_le : round (a + b) ≤ a + b
size_eq : Nat.size (a + b) = Nat.size a
ulp_eq : ulp n (a + b) = ulp n a
mod_ulp₁ : a % ulp n a = 0
mod_ulp₂ : (a + b) % ulp n a = b % ulp n a
error_eq : a + b - trunc n (a + b) = b % ulp n a
⊢ ulp n b ∣ b
Tactic:
exact ulp_dvd_of_trunc_eq hfb
State after:
no goals