0.96:ℚ * n < 1.0:ℚ * n - why so difficult? (with MWE)

Stream: new members

[rzeta0]

As part of a wider proof, in a calc section I'm trying to show: 0.6:ℚ * n < 1.0:ℚ * n where n:ℕ

_ < ((F (k + 1)):ℚ) + 0.96 * ((F k):ℚ) := by rel [ih2a, ih1a]
_ < ((F (k + 1)):ℚ) + ((F k):ℚ) := by norm_num -- < -- problem line

Ive tried to create some MWEs

Without variables, this works:

example : (0.4 : ℚ) < (1:ℚ) :=
  calc
    (0.4 : ℚ) < (1 : ℚ) := by norm_num

With a variable however, I can't seem to justify what in my brain feels like a trivial fact:

example : ∀ n:ℕ, (0.9: ℚ) * n < (1:ℚ) * n := by
  intro n
  calc
    (0.9 : ℚ) * n < (1 : ℚ) * n := by norm_num --< -- fails

Interestingly it says the unsolved goal is 9 / 10 * ↑n < ↑n. I hope I don't need to invoke lemmas like mul_lt_mul_of_pos_right.

I even tried horrible tricks like this which sometimes work:

example : ∀ n:ℕ, (0.9: ℚ) * n < (1:ℚ) * n := by
  intro n
  calc
    (0.9 : ℚ) * n < (0.9 + 0.1 : ℚ) * n := by norm_num -- < fails --
    _ = (1 : ℚ) * n := by norm_num

I've tried other tactics but none work - note linarith is disabled in MoP.

[Etienne Marion]

It does not hold if n=0, because in that case both sides are 0 so the inequality is not strict

[rzeta0]

Thanks Etienne - my brain is not working today. :)

[Riccardo Brasca]

Anyway the tactic you want (meaning it finds mul_lt_mul_of_pos_right or something like that) is gcongr