Fluxes Ten chiral Indices Of U noneg of no Exotics

lemma FluxesTen.chiralIndicesOfU_noneg_of_noExotics (F : FluxesTen) (hF : NoExotics F)    (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfU) : 0 ≤ ci := by  by_contra hn  simp only [not_le] at hn  have hF1 := hF.2.2.2  simp [numAntiChiralU] at hF1  have h1 := Multiset.sum_le_card_nsmul    (Multiset.filter (fun x => x < 0) F.chiralIndicesOfU) (-1)    (fun x hx => by      have := (Multiset.mem_filter.mp hx).2      omega)  rw [nsmul_eq_mul] at h1  have h2 : 0 < Multiset.card (Multiset.filter (fun x => x < 0) F.chiralIndicesOfU) :=    Multiset.card_pos_iff_exists_mem.mpr ⟨ci, Multiset.mem_filter.mpr ⟨hci, hn⟩⟩  omega