Add theorem "elements_remove".

Use "elements_remove" to simplify the proof of "cardinal_remove".
Simplify some of the proofs over function "xelements".