proposition: Lemma size_rembig w : size (rembig w) = (size w).-1.
proof: Proof. Proof using. elim: w => //= a w IHw. case: w IHw => [//= | b w'] IHw. by case (allLtn (b :: w') a); rewrite //= IHw. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools