proposition: Lemma sumn_rem_trail0 s : sumn (rem_trail0 s) = sumn s.
proof: Proof. elim: s => //= s0 s. case: (rem_trail0 s) => [/= <- | t1 t' <- //=]. by case: (s0 =P 0%N) => [-> | _] /=; rewrite ?addn0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype