proposition: Lemma set_CSm A B X: sub A X -> sub B X -> (sub A B <-> sub (X -s B) (X -s A)).
proof: Proof. move=> ax bx; split; first by apply: set_CS. by move => h; rewrite -(setC_K ax) -(setC_K bx); apply: set_CS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)