Description: Lemma for the equality theorem for partition ~? parteq1 . (Contributed by Peter Mazsa, 5-Oct-2021)