proposition: Theorem comb_id : ∀ n, comb n n = 1%nat.
proof: Proof. intros n. induction n; [ reflexivity | simpl ]. rewrite IHn, comb_lt; [ idtac | apply Nat.lt_succ_r; reflexivity ]. rewrite Nat.add_0_r; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn