mathlib3

24a1af3d - Fixed proof of `disjoint_prod_add_aux`