Pair Rel Dist le iff pair Dist le

lemma pairRelDist_le_iff_pairDist_le (δ : NNReal) :    (δᵣ(u, v) ≤ δ) ↔ (Δ₀(u, v) ≤ Nat.floor (δ * Fintype.card ι)) := by  -- 1. Get n > 0 from [Nonempty ι]  have h_n_pos : 0 < Fintype.card ι := Fintype.card_pos  have h_n_pos_nnreal : 0 < (Fintype.card ι : NNReal) := by exact_mod_cast h_n_pos  -- 2. Unfold the definition and handle the coercion from ℚ≥0 to NNReal  unfold relHammingDist  simp only [NNRat.cast_div, NNRat.cast_natCast]  conv_lhs => change (Δ₀(u, v) : ℝ≥0) / (Fintype.card ι : ℝ≥0) ≤ δ  conv_rhs => change Δ₀(u, v) ≤ Nat.floor ((δ : ℝ) * (Fintype.card ι : ℝ))  conv_lhs => rw [div_le_iff₀ (by exact_mod_cast h_n_pos)]  conv_rhs => simp [Nat.le_floor_iff]  rfl