Rq l2Norm Sq sub le

theorem Rq.l2NormSq_sub_le (a b : Rq Φ) :    ‖a - b‖₂² ≤ 2 * (‖a‖₂² + ‖b‖₂²) := by  unfold Rq.l2NormSq  rw [← Finset.sum_add_distrib, Finset.mul_sum]  refine Finset.sum_le_sum (fun k _ => ?_)  have hcoeff : (a - b).1.coeff k = a.1.coeff k - b.1.coeff k := by    rw [Rq.sub_val, CompPoly.CPolynomial.coeff_sub]  rw [hcoeff]  have htri := valMinAbs_sub_natAbs_le (a.1.coeff k) (b.1.coeff k)  have htriZ : ((a.1.coeff k - b.1.coeff k).valMinAbs.natAbs : ℤ)      ≤ (a.1.coeff k).valMinAbs.natAbs + (b.1.coeff k).valMinAbs.natAbs := by exact_mod_cast htri  have key : ((a.1.coeff k - b.1.coeff k).valMinAbs.natAbs : ℤ) ^ 2      ≤ 2 * (((a.1.coeff k).valMinAbs.natAbs : ℤ) ^ 2        + ((b.1.coeff k).valMinAbs.natAbs : ℤ) ^ 2) := by    nlinarith [htriZ, Int.natCast_nonneg (a.1.coeff k - b.1.coeff k).valMinAbs.natAbs,      sq_nonneg (((a.1.coeff k).valMinAbs.natAbs : ℤ) - (b.1.coeff k).valMinAbs.natAbs)]  exact_mod_cast key