proposition: Lemma rcons_nilF s l : ((rcons s l) == [::]) = false.
proof: Proof. Proof using. by apply/negbTE/negP => /eqP/(congr1 size); rewrite size_rcons. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)