proposition: Lemma setU1_K A b: ~(inc b A) -> (A +s1 b) -s1 b = A.
proof: Proof. move => nba; set_extens t;first by case /setC1_P; case /setU1_P. move => tA; apply/setC1_P; split; [fprops | dneg ta;ue ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)