dsimp only [primesBetween]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ primesBetween a b ≤ primesBetween a c
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b c : ℝ
hbc : b ≤ c
⊢ (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊b⌋₊)).card ≤ (Finset.filter Nat.Prime (Finset.Icc ⌈a⌉₊ ⌊c⌋₊)).card