proposition: Lemma setC1_eq A x: ~(inc x A) -> A -s1 x = A.
proof: Proof. move=> h. set_extens t; first by move => /setC1_P []. by move => tA; apply /setC1_P; split => // tx; case: h; rewrite - tx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)