feat: a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n (#20577) From GrowthInGroups (LeanCamCombi)
a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n