BohrSet.chordSet_subset_smul_arcSet

lemma chordSet_subset_smul_arcSet [Finite G] :    B.chordSet ⊆ ((π / 2) • B).arcSet := fun x hx ψ => by  rw [ewidth_smul]  split  case isFalse => simp  case isTrue h =>    have := hx ψ    simp only [←coe_width h, ENNReal.coe_le_coe, ←ENNReal.coe_mul, ←NNReal.coe_le_coe,      coe_nnnorm, NNReal.coe_mul] at this ⊢    rw [coe_nnabs, abs_of_nonneg pi_div_two_pos.le, Real.norm_of_nonneg (angle_nonneg _ _),      angle_comm]    refine (Complex.angle_le_mul_norm_sub (by simp) (by simp)).trans ?_    gcongr