feat(data/int/basic): Sum of units casework lemma (#14557)
This PR adds a casework lemma for when the sum of two units equals the sum of two units. I needed this lemma for irreducibility of x^n-x-1.
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
