proposition: Theorem comb_lt : ∀ n k, (n < k)%nat → comb n k = 0%nat.
proof: Proof. intros n k Hnk. revert k Hnk. induction n; intros; simpl. destruct k; [ exfalso; revert Hnk; apply Nat.nlt_0_r | auto ]. destruct k; [ exfalso; revert Hnk; apply Nat.nlt_0_r | auto ]. apply Nat.succ_lt_mono in Hnk. rewrite IHn; [ idtac | assumption ]. rewrite IHn; [ reflexivity | idtac ]. apply Nat.lt_lt_succ_r; assumption. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn