Theorem: IMOSL.IMO2006A1.case_floor_eventually_neg_of_one_lt (IMOSLLean4/IMO2006/A1/A1.lean)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
rcases h with ⟨N, _, h⟩
State after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋) (k + N) = (fun x => -↑C) (k + w✝)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε

State before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋) (k + N) = (fun x => -↑C) (k + w✝)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
simp only at h
State after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε

State before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
have h0 (k) : (C + 1) * f^[(k + 1) + N] r + C ^ 2
    = -C * ((C + 1) * f^[k + N] r + C ^ 2) := by
  have h0 := f_alt_formula (f^[k + N] r)
  rw [h, Int.cast_neg, Int.cast_natCast, neg_sq, ← neg_add', neg_mul, ← neg_add',
    neg_mul, neg_inj, neg_mul, ← neg_add', mul_neg, ← neg_mul] at h0
  rwa [Nat.add_right_comm, f.iterate_succ_apply']
State after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε

State before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
replace h0 : ∀ k, (C + 1) * f^[k + N] r + C ^ 2
    = (-C) ^ k * ((C + 1) * f^[N] r + C ^ 2) :=
  Nat.rec (by rw [Nat.zero_add, pow_zero, one_mul])
    (λ k h1 ↦ by rw [h0, h1, ← mul_assoc, ← pow_succ'])
State after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ((↑C + 1) * f^[N] r + ↑C ^ 2)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε

State before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ((↑C + 1) * f^[N] r + ↑C ^ 2)
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
set ε := (C + 1) * f^[N] r + C ^ 2
State after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε

State before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
refine ⟨ε, ?_, N, 0, λ k ↦ eq_neg_add_of_add_eq <| (add_comm _ _).trans (h0 k)⟩
State after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ Infinitesimal ε

State before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ Infinitesimal ε
Tactic:
replace h0 (k) : |(C + 1) * Int.fract (f^[k + N] r) - C| = C ^ k • |ε| := by
  specialize h0 k
  rw [sq, ← Int.fract_add_floor (f^[k + N] r), h, Int.cast_neg, Int.cast_natCast, mul_add,
    mul_neg, add_one_mul (C : R) C, add_assoc, neg_add_rev, neg_add_cancel_right] at h0
  rw [sub_eq_add_neg, h0, abs_mul, abs_pow, abs_neg,
    Nat.abs_cast, nsmul_eq_mul, Nat.cast_pow]
State after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
⊢ Infinitesimal ε

State before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
⊢ Infinitesimal ε
Tactic:
replace h (s : R) : |(C + 1) * Int.fract s - C| < ((C + 1 + C : ℕ) : R) := by
  apply (abs_sub _ _).trans_lt
  rw [Nat.abs_cast, Nat.cast_add, add_lt_add_iff_right, ← Nat.cast_succ,
    abs_mul, Nat.abs_cast, abs_eq_self.mpr (Int.fract_nonneg s)]
  refine mul_lt_of_lt_one_right (Nat.cast_pos.mpr C.succ_pos) (Int.fract_lt_one _)
State after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
h : ∀ (s : R), |(↑C + 1) * Int.fract s - ↑C| < ↑(C + 1 + C)
⊢ Infinitesimal ε

State before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
h : ∀ (s : R), |(↑C + 1) * Int.fract s - ↑C| < ↑(C + 1 + C)
⊢ Infinitesimal ε
Tactic:
exact Infinitesimal.iff_nsmul_Nat_bdd.mpr ⟨C + 1 + C, λ k ↦
  (nsmul_le_nsmul_left (abs_nonneg ε) (Nat.lt_pow_self hC k).le).trans_lt <|
    (h0 _).symm.trans_lt (h (f^[k + N] r))⟩
State after:
no goals

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
k : ℕ
⊢ (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
Tactic:
have h0 := f_alt_formula (f^[k + N] r)
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
k : ℕ
h0 :
  (↑⌊f^[k + N] r⌋ - 1) * f (f^[k + N] r) - ↑⌊f^[k + N] r⌋ ^ 2 =
    ↑⌊f^[k + N] r⌋ * ((↑⌊f^[k + N] r⌋ - 1) * f^[k + N] r - ↑⌊f^[k + N] r⌋ ^ 2)
⊢ (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
k : ℕ
h0 :
  (↑⌊f^[k + N] r⌋ - 1) * f (f^[k + N] r) - ↑⌊f^[k + N] r⌋ ^ 2 =
    ↑⌊f^[k + N] r⌋ * ((↑⌊f^[k + N] r⌋ - 1) * f^[k + N] r - ↑⌊f^[k + N] r⌋ ^ 2)
⊢ (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
Tactic:
rw [h, Int.cast_neg, Int.cast_natCast, neg_sq, ← neg_add', neg_mul, ← neg_add',
  neg_mul, neg_inj, neg_mul, ← neg_add', mul_neg, ← neg_mul] at h0
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
k : ℕ
h0 : (↑C + 1) * f (f^[k + N] r) + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
⊢ (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
k : ℕ
h0 : (↑C + 1) * f (f^[k + N] r) + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
⊢ (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
Tactic:
rwa [Nat.add_right_comm, f.iterate_succ_apply']
State after:
no goals

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
⊢ (↑C + 1) * f^[Nat.zero + N] r + ↑C ^ 2 = (-↑C) ^ Nat.zero * ((↑C + 1) * f^[N] r + ↑C ^ 2)
Tactic:
rw [Nat.zero_add, pow_zero, one_mul]
State after:
no goals

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + 1 + N] r + ↑C ^ 2 = -↑C * ((↑C + 1) * f^[k + N] r + ↑C ^ 2)
k : ℕ
h1 : (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ((↑C + 1) * f^[N] r + ↑C ^ 2)
⊢ (↑C + 1) * f^[k.succ + N] r + ↑C ^ 2 = (-↑C) ^ k.succ * ((↑C + 1) * f^[N] r + ↑C ^ 2)
Tactic:
rw [h0, h1, ← mul_assoc, ← pow_succ']
State after:
no goals

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
k : ℕ
⊢ |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
Tactic:
specialize h0 k
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
k : ℕ
h0 : (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
k : ℕ
h0 : (↑C + 1) * f^[k + N] r + ↑C ^ 2 = (-↑C) ^ k * ε
⊢ |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
Tactic:
rw [sq, ← Int.fract_add_floor (f^[k + N] r), h, Int.cast_neg, Int.cast_natCast, mul_add,
  mul_neg, add_one_mul (C : R) C, add_assoc, neg_add_rev, neg_add_cancel_right] at h0
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
k : ℕ
h0 : (↑C + 1) * Int.fract (f^[k + N] r) + -↑C = (-↑C) ^ k * ε
⊢ |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
k : ℕ
h0 : (↑C + 1) * Int.fract (f^[k + N] r) + -↑C = (-↑C) ^ k * ε
⊢ |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
Tactic:
rw [sub_eq_add_neg, h0, abs_mul, abs_pow, abs_neg,
  Nat.abs_cast, nsmul_eq_mul, Nat.cast_pow]
State after:
no goals

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
s : R
⊢ |(↑C + 1) * Int.fract s - ↑C| < ↑(C + 1 + C)
Tactic:
apply (abs_sub _ _).trans_lt
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
s : R
⊢ |(↑C + 1) * Int.fract s| + |↑C| < ↑(C + 1 + C)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
s : R
⊢ |(↑C + 1) * Int.fract s| + |↑C| < ↑(C + 1 + C)
Tactic:
rw [Nat.abs_cast, Nat.cast_add, add_lt_add_iff_right, ← Nat.cast_succ,
  abs_mul, Nat.abs_cast, abs_eq_self.mpr (Int.fract_nonneg s)]
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
s : R
⊢ ↑C.succ * Int.fract s < ↑(C + 1)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
hC : 1 < C
N w✝ : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = -↑C
ε : R := (↑C + 1) * f^[N] r + ↑C ^ 2
h0 : ∀ (k : ℕ), |(↑C + 1) * Int.fract (f^[k + N] r) - ↑C| = C ^ k • |ε|
s : R
⊢ ↑C.succ * Int.fract s < ↑(C + 1)
Tactic:
refine mul_lt_of_lt_one_right (Nat.cast_pos.mpr C.succ_pos) (Int.fract_lt_one _)
State after:
no goals