proposition: Lemma subsetC1_P A B x: (sub A (B -s1 x)) <-> (sub A B /\ ~inc x A).
proof: Proof. split; first by case/subCset_P3=> [pa pb]; split => // xa; empty_tac1 x; fprops. move => [pa pb] t ta; apply/setC1_P; split; fprops; dneg tx; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)