proposition: Theorem comb_0_r : ∀ i, comb i 0 = 1%nat.
proof: Proof. intros i; destruct i; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn