proposition: Lemma undup_rcons s x : undup (rcons s x) = rcons [seq y <- undup s | y != x] x.
proof: Proof. by rewrite -!cats1 undup_cat; congr cat; apply: eq_filter => y; rewrite inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)