proposition: Lemma setU1_finite X x: finite_set X -> finite_set (X +s1 x).
proof: Proof. move=>fX; case: (inc_or_not x X) => h; first by rewrite (setU1_eq h). rewrite/finite_set (csucc_pr h); apply /finite_succP; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)