fact: Fixpoint rem_trail0 s := if s is s0 :: s' then if (rem_trail0 s') is t1 :: t' then s0 :: t1 :: t' else if s0 == 0 then [::] else [:: s0] else [::].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype