proposition: Lemma complement_p1 C A B: A \cup B = C -> A \cap B = emptyset -> (sub A C /\ A = C -s B).
proof: Proof. move => uab iab. have sa: sub A C by move=> t tA; rewrite -uab; fprops. have sb: sub B C by move=> t tB; rewrite -uab; fprops. split => //; set_extens t. move=> tA; apply /setC_P;split => //; first by apply: sa. by move=> tB; empty_tac1 t; apply: setI2_i. rewrite - uab; move /setC_P => [tc tb]; case /setU2_P: tc => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)