mathlib3

b00a5ba7 - Rename to `prod_add_index_of_disjoint`; reverse order of equality