proposition: Lemma setC_K A B: sub A B -> B -s (B -s A) = A.
proof: Proof. move=> sax; set_extens t. by move /setC_P => [tx /setC_P notp];ex_middle h; case: notp. move =>ta; apply/setC_P; split; [apply: (sax _ ta) | by apply/setC_P; case ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)