proposition: Lemma intpart_sumn_take_inj (s t : intpart) : (forall k, sumn (take k s) = sumn (take k t)) -> s = t.
proof: Proof. move=> H; apply: val_inj => /=. by apply: sumn_take_inj; last exact H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype