f g : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑n * ↑⌊↑f 0⌋ ≤ (↑f^[n]) 0
f g : CircleDeg1Lift
n : ℕ
⊢ ↑n * ⌊↑f 0⌋ ≤ ⌊(↑f^[n]) 0⌋
rw [le_floor, Int.cast_mul, Int.cast_ofNat, ← zero_add ((n : ℝ) * _)]
case h
f g : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑⌊↑f 0⌋ ≤ ↑f 0
f g : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑n * ↑⌊↑f 0⌋ ≤ (↑f^[n]) 0
apply le_iterate_of_add_int_le_map
no goals
case h
f g : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑⌊↑f 0⌋ ≤ ↑f 0
simp [floor_le]