Card constraint Indices

lemma card_constraintIndices (m : ℕ) : (constraintIndices m).card = m * (m + 1) / 2 := by  rw [Nat.div_eq_of_eq_mul_left zero_lt_two]  have h_eq : (constraintIndices m).card = ∑ s ∈ range m, (m - s) := by    have h_sum : (constraintIndices m).card = ∑ s ∈ range m, (range (m - s)).card := by      rw [show constraintIndices m = (range m).biUnion fun s ↦        (range (m - s)).image (fun t ↦ (s, t))  from ?_, card_biUnion]      · exact sum_congr rfl fun _ _ ↦          card_image_of_injective _ fun _ _ h ↦ by exact Prod.ext_iff.mp h |>.2      · exact fun i hi j hj hij ↦ disjoint_left.mpr fun x hx₁ hx₂ ↦ hij <| by aesop      · ext ⟨s, t⟩        simp [constraintIndices, mem_biUnion, mem_image]        omega    aesop  exact h_eq.symm ▸ Nat.recOn m (by norm_num) fun n ih ↦ by    cases n <;> simp [sum_range_succ', Nat.mul_succ] at *    linarith