proposition: Lemma rembig_rev_uniq s : uniq s -> rev (rembig s) = rembig (rev s).
proof: Proof. Proof using. case: (s =P [::]) => [-> //= |]. move=> /eqP/rembigP/(_ (eq_refl (rembig s))) [u] [b] [v] [] -> -> Hu Hb. rewrite -rev_uniq !rev_cat rev_cons -cats1 -catA cat1s. rewrite cat_uniq => /and3P[_ _ /= /andP[]]. rewrite mem_rev => Hbu _. apply/eqP/rembigP; first by case: (rev v). exists (rev v), b, (rev u); split => //. - by rewrite allLeq_rev; apply: allLtnW. - by rewrite allLtn_rev; apply: allLtn_notin. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools