proposition: Lemma setC1_P x A b: inc x (A -s1 b) <-> (inc x A /\ x <> b).
proof: Proof. split; first by case /setC_P => xa /set1_P xb. by move => [xA xb]; apply /setC_P; split => //;apply /set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)