proposition: Lemma nth_diff_shape inn out i : nth 0 (out / inn) i = nth 0 out i - nth 0 inn i.
proof: Proof. elim: inn out i => [| inn0 inn IHinn] out i /=. by rewrite (@nth_default _ _ [::]) // subn0. case: out => [| out0 out] /=. by rewrite nth_default. by case: i => [| i] /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype