Lean simp as bubble sort for anticommuting ring elements (Clifford products)

To prove identities like star(b0*b1*b2) = -(b0*b1*b2) or (b_r*ω)^2 = -1 for pairwise anticommuting b_i with b_i*b_i = 1 in a noncommutative ring, noncomm_ring cannot use the hypotheses and a general anticommute lemma makes simp loop. What worked: state ORIENTED conditional rules hbb (r s : Fin 4) (h : r < s) : b s * b r = -(b r * b s) plus right-associated versions x * (y * z) = -(y * (x * z)) (one-line lemma: rw [← mul_assoc, h, neg_mul, mul_assoc]) and squares x * (x * z) = z, then simp only [mul_assoc, star_mul, ...]; fin_cases r <;> simp [hbb, hbb', hs, hs']. simp discharges the r < s side conditions on Fin literals itself, and the rule set terminates (it is a bubble sort with signs). Mixed families: orient a_i before b_j with b j * a i = -(a i * b j).