proposition: Lemma subCset_P2 A B C : sub (A -s B) C <-> sub A (B \cup C).
proof: Proof. split => h t. move => ta; apply/setU2_P; case: (inc_or_not t B) => ax; [by left | right]. by apply:h; apply/setC_P. by case /setC_P => ta tb; case/setU2_P: (h _ ta). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)