proposition: Lemma disjoint_subsets_P A E: sub A E -> forall B, (disjoint A B <-> sub A (E -s B)).
proof: Proof. move => sae B; split. move => dab t ta; apply/setC_P; split; first by apply: sae. move => tb;empty_tac1 t. by move => sd; apply: disjoint_pr => u ua; move: (sd _ ua); case /setC_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)