Rel Hamming Dist le block Rel Distance

lemma relHammingDist_le_blockRelDistance (hkn : k ≤ n) :  δᵣ(f, g) ≤ δ𞁒(k, φ, f, g) := by  apply le_trans  · exact relHammingDist_le_sub_agreementBlockUnion      (f := f) (g := g) (φ := φ) (k := k)  · rw [card_agreementBlockUnion hkn]    rw [Nat.cast_mul]    simp only [Nat.cast_pow, Nat.cast_ofNat]    have : (Nat.cast (2 : ℕ) ^ n : ℚ≥0) = (Nat.cast <| 2 ^ k * 2 ^ (n - k)) := by      rw [←Nat.pow_add, Nat.add_sub_of_le hkn]      simp    rw [show (2 : ℚ≥0) ^ n = (((2 : ℕ) ^ n) : ℚ≥0) by rfl, this, Nat.cast_mul]    simp only [Nat.cast_pow, Nat.cast_ofNat, tsub_le_iff_right, ge_iff_le]    conv_rhs =>      rhs      field_simp    rw [blockRelDistance_eq_one_sub]    simp only [card_toFinset, Fintype.card_fin, Nat.cast_pow, Nat.cast_ofNat]    rw [←NNRat.coe_le_coe]    simp only [NNRat.cast_one, NNRat.cast_add, NNRat.cast_div, NNRat.cast_natCast, NNRat.cast_pow,      NNRat.cast_ofNat]    rw [NNRat.coe_sub (by aesop (add safe [(by field_simp), (by norm_cast)]))]    simp