proposition: Theorem comb_1_r : ∀ n, comb n 1 = n.
proof: Proof. intros n. induction n; [ reflexivity | simpl ]. rewrite comb_0_r, IHn; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn