proposition: Lemma rconsK a b u v : rcons u a = rcons v b -> u = v.
proof: Proof. Proof using. by move/(congr1 rev); rewrite !rev_rcons => [[_ /(inv_inj revK)]]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)