proposition: Lemma Exercise5_3c n k p: natp n -> natp p -> k <=c p -> Exercise5_3V n p k = (binom p k) *c (binom n p).
proof: Proof. rewrite /Exercise5_3V => nN pN lkp. have kN := NS_le_nat lkp pN. move:(NS_diff k nN) (NS_diff k pN) => nkN pkN. case: (NleT_el pN nN) => lpn; last first. rewrite (binom_bad nN pN lpn) cprod0r. case: (NleT_el kN nN) => lkn. have l2: (n -c k) <c (p -c k) by apply (cdiff_pr7 lkn lpn pN). by rewrite (binom_bad nkN pkN l2) cprod0r. by rewrite (binom_bad nN kN lkn) cprod0l. have lkn:= cleT lkp lpn. have l3: (p -c k) <=c (n -c k). case: (equal_or_not p n) => epn; first by rewrite epn; fprops. exact: (proj1 (cdiff_pr7 lkp (conj lpn epn) nN)). have npN := NS_diff p nN. have ha:=(binom_good nN kN lkn). have hb:=(binom_good nkN pkN l3). have hc:=(binom_good pN kN lkp). have hd:=(binom_good nN pN lpn). have x1N: natp (binom n k *c binom (n -c k) (p -c k)). by apply:NS_prod; apply:NS_binom. have x2N: natp (binom p k *c binom n p) by apply:NS_prod; apply:NS_binom. have x3N: natp ((factorial k) *c factorial (n -c k)). by apply:NS_prod; apply:NS_factorial. have x3z: ((factorial k) *c factorial (n -c k)) <> \0c. by apply: cprod2_nz; apply: factorial_nz. have x4N: natp (binom (n -c k) (p -c k) *c factorial n). by apply:NS_prod; [ apply: NS_binom | apply:NS_factorial]. have fpkN:=(NS_factorial pkN). have x5N:natp (binom n p *c (factorial p *c factorial (n -c k))). by apply:NS_prod; [ apply:NS_binom | apply: NS_prod; apply:NS_factorial]. have sa:((n -c k) -c (p -c k)) = n -c p. by have d1:= (cdiff_pr lkp); rewrite (cdiffA nN kN pkN) d1. rewrite sa in hb. apply: (cprod_eq2r x3N x1N x2N x3z). rewrite (cprodC (binom n k)) - cprodA ha. apply:(cprod_eq2r fpkN x4N (NS_prod x2N x3N) (factorial_nz pkN)). rewrite (cprodC (binom p k)) cprodA -3!(cprodA (binom n p)). set x := (binom p k *c factorial k). rewrite - (cprodA x) (cprodC (factorial (n -c k))) (cprodA x) /x. rewrite - (cprodA (binom p k)) hc. apply:(cprod_eq2r (NS_factorial npN) (NS_prod x4N fpkN) x5N (factorial_nz npN)). set y:=(factorial n); rewrite (cprodC _ y) -(cprodA y) - {1} (cprodA y). rewrite - (cprodA (binom _ _)) hb cprodA - cprodA. by rewrite (cprodC (factorial (n -c k))) cprodA - (cprodA (binom n p)) hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)