add lemma about chained difference

Merged Ralf Jung requested to merge ralf/difference_union into master

Merge request reports