proposition: Lemma complement_p3 C B (A:= C -s B): sub B C -> (A \cup B = C /\ A \cap B = emptyset).
proof: Proof. move=> BC; rewrite /A;split. set_extens t. case /setU2_P; [ by move => /setC_P [] | apply: BC ]. move => tC; case:(inc_or_not t B) => tB; apply /setU2_P; [right | left] =>//. by apply /setC_P. by apply /set0_P => y /setI2_P [] /setC_P []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)