proposition: Lemma subsets_disjoint_P A B E: sub A E -> (sub A B <-> disjoint A (E -s B)).
proof: Proof. move => ae;split. by move => ab; apply: disjoint_pr => u ua; case /setC_P; move: (ab _ ua). move => dae t ta; ex_middle tb; empty_tac1 t; apply/setC_P; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)