proposition: Lemma binom_add_INC : forall n k : nat, (n>= k)%nat -> - INC (fact n) / INC (fact (n-k) * fact k) + INC (fact (S n)) / INC (fact k * fact (S (n - k))) = INC (k * fact n) / INC ( fact k * fact (S (n-k))).
proof: Proof. intros n k H. do 2 rewrite fact_simpl. replace (INC (fact k * (S (n - k) * fact (n - k)))) with (INC (S (n-k)) * INC (fact k * fact (n-k))) by (rewrite Nat.mul_comm ; symmetry ; rewrite Nat.mul_comm ; rewrite <- mult_INC ; rewrite Nat.mul_assoc ; reflexivity). replace (INC (S n * fact n)) with (INC (S n) * INC (fact n)) by (rewrite mult_INC ; reflexivity). unfold Cdiv. rewrite Cinv_mult_distr. apply (Cmult_eq_reg_l (INC (S (n - k)))). apply not_0_INC. intuition lia. rewrite Cmult_add_distr_l. repeat rewrite mult_INC. field_simplify. rewrite Cmult_comm. rewrite <- Cmult_add_distr_l. unfold Cdiv. repeat rewrite Cmult_assoc. apply Cmult_eq_compat_l. rewrite Cadd_comm. replace (INC (S n) + - INC (S (n - k))) with (INC (S n) - INC (S (n - k))) by intuition. rewrite <- minus_INC. simpl. rewrite minus_INC. rewrite minus_INC. ring. lia. lia. lia. split. apply not_0_INC. apply fact_neq_0. split. apply not_0_INC. apply fact_neq_0. apply not_0_INC. intuition lia. split. apply not_0_INC. apply fact_neq_0. split. apply not_0_INC. apply fact_neq_0. apply not_0_INC. intuition lia. apply not_0_INC. intuition lia. apply not_0_INC. intro Habs. apply Nat.eq_mul_0 in Habs. elim Habs; apply fact_neq_0. Qed.
imports: Ctacfield Cbase Cprop_base Cfunctions Cpow Lia