proposition: Lemma setCU_K A B: sub B A <-> (A -s B) \cup B = A.
proof: Proof. split; last by move => h t tb; rewrite -h; apply/setU2_P; right. move => BA; set_extens t; first by case /setU2_P; [ by case/setC_P| apply: BA]. move => tA; apply/setU2_P; case: (inc_or_not t B) => ty;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)