proposition: Lemma not_memX (ks : seq nat) : exists k, k \notin ks.
proof: Proof. have L a xs : foldl addn a xs = a + foldl addn 0 xs. - elim: xs a=>[|z xs IH] //= a; first by rewrite addn0. by rewrite add0n // [in LHS]IH [in RHS]IH addnA. set k := foldl addn 1 ks. suff K a : a \in ks -> a < k by exists k; apply/negP=>/K; rewrite ltnn. rewrite {}/k; elim: ks=>[|k ks IH] //=; rewrite inE. case/orP=>[/eqP ->|/IH]; first by rewrite L add1n addSn ltnS leq_addr. rewrite L=>N; rewrite L; apply: leq_trans N _. by rewrite addnAC leq_addr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)