proposition: Lemma is_part_rem_trail0 s : sorted geq s -> is_part (rem_trail0 s).
proof: Proof. case: s => [// | s0 s]; rewrite [sorted _ _]/=. elim: s s0 => [| s1 s IHs] s0 /=; first by case: s0. move=> /andP[H01 /IHs /=]. case: (rem_trail0 s) => [_ | t0 t] /=; last by rewrite H01. case: (s1 =P 0) => [_ | /eqP Hs1]. - case (s0 =P 0) => [// | /eqP Hs0] /=. by rewrite lt0n Hs0. - by rewrite /= H01 lt0n Hs1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype