proposition: Lemma setU2Cr2 A B: A \cup (B -s A) = A \cup B.
proof: Proof. set_extens t; case /setU2_P => t1; apply/setU2_P; fprops. by right;case /setC_P:t1. case: (inc_or_not t A)=> ta; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)