proposition: Lemma size_rem_trail0 s : size (rem_trail0 s) <= size s.
proof: Proof. by elim: s => //= s0 s; case: (rem_trail0 s) => //= _; case: eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype