proposition: Lemma nth_rem_trail0 s i : nth 0 (rem_trail0 s) i = nth 0 s i.
proof: Proof. elim: s i => //= s0 s. case: (rem_trail0 s) => [/= | t1 t'] IHs i. - by case (s0 =P 0) => [-> | _]; case: i => //= i; rewrite -IHs. - by case: i => //= i; apply: IHs. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype