Rq eq zero of l2Norm Sq eq zero

theorem Rq.eq_zero_of_l2NormSq_eq_zero {c : Rq Φ} (h : Rq.l2NormSq Φ c = 0) : c = 0 := by  unfold Rq.l2NormSq at h  -- Each centered coefficient below `deg φ` is zero.  have hlt : ∀ k, k < (powTwoCyclotomic (R := ZMod q) α).φ.natDegree → c.1.coeff k = 0 := by    intro k hk    have hsq : (c.1.coeff k).valMinAbs.natAbs ^ 2 = 0 :=      (Finset.sum_eq_zero_iff.mp h) k (Finset.mem_range.mpr hk)    have hz0 : (c.1.coeff k).valMinAbs.natAbs = 0 := (Nat.pow_eq_zero.mp hsq).1    rw [← ZMod.valMinAbs_eq_zero, ← Int.natAbs_eq_zero]    exact hz0  -- Hence the underlying polynomial is `0` (coeffs below `deg φ` by the above, coeffs at or  -- above `deg φ` by reducedness).  have htoP : c.1.toPoly = 0 := by    apply Polynomial.ext    intro k    rw [Polynomial.coeff_zero]    by_cases hk : k < (powTwoCyclotomic (R := ZMod q) α).φ.natDegree    · rw [← CompPoly.CPolynomial.coeff_toPoly]; exact hlt k hk    · rw [not_lt] at hk      have hdeg : c.1.toPoly.degree < (powTwoCyclotomic (R := ZMod q) α).φ.toPoly.degree :=        (powTwoCyclotomic (R := ZMod q) α).degree_toPoly_lt_of_reduced c.2      have hmonic : (powTwoCyclotomic (R := ZMod q) α).φ.toPoly.Monic := IsCyclotomic.monic      have hφne : (powTwoCyclotomic (R := ZMod q) α).φ.toPoly ≠ 0 := hmonic.ne_zero      have hdegφ : (powTwoCyclotomic (R := ZMod q) α).φ.toPoly.degree          = ((powTwoCyclotomic (R := ZMod q) α).φ.natDegree : WithBot ℕ) := by        rw [Polynomial.degree_eq_natDegree hφne, CompPoly.CPolynomial.natDegree_toPoly]      have hle' : (powTwoCyclotomic (R := ZMod q) α).φ.toPoly.degree ≤ (k : WithBot ℕ) := by        rw [hdegφ]; exact_mod_cast hk      exact Polynomial.coeff_eq_zero_of_degree_lt (lt_of_lt_of_le hdeg hle')  have hc1 : c.1 = 0 := (CompPoly.CPolynomial.toPoly_eq_zero_iff c.1).mp htoP  exact Subtype.ext (by rw [Rq.zero_val]; exact hc1)