deduplicate opposite argument in ideals for ideal_produc_assoc

We show that the opposite of product ideals is the opposite of the
reverse product. This allows us to deduplicate the argument occuring in
ideal_product_assoc. In order to do this we need to move some things
around and explode the Section IdealLemmas.

Signed-off-by: Ali Caglayan <[email protected]>

Author: Alizter