50theorem flameSpeed_strictly_increasing (k : ℕ) : 51 flameSpeed k < flameSpeed (k + 1) := by
proof body
Tactic-mode proof.
52 rw [flameSpeed_succ_ratio] 53 have hk : 0 < flameSpeed k := flameSpeed_pos k 54 have hphi_gt_one : (1 : ℝ) < phi := by 55 have := Constants.phi_gt_onePointFive; linarith 56 have : flameSpeed k * 1 < flameSpeed k * phi := by 57 apply mul_lt_mul_of_pos_left hphi_gt_one hk 58 simpa using this 59 60/-- Adjacent-rung flame-speed ratio equals φ. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.