proposition: Lemma binom_alt_pr n m: natp n -> natp m -> (binom n m) *c ((factorial m) *c (factorial (n -c m))) = Yo (m <=c n) (factorial n) \0c.
proof: Proof. move: n m. pose Bi n m := (binom n m) *c (factorial m *c (factorial (n -c m))). have ba4: forall n m, natp n -> natp m -> Bi (csucc n) (csucc m)= ((Bi n (csucc m)) *c (Yo (n <=c m) \1c (n -c m))) +c (Bi n m *c csucc m). move=> n m nN mN. rewrite /Bi binomSnSm // cdiff_pr6 // cprodDl. set aux := (factorial (csucc m)) *c (factorial (n -c m)). set A:= (binom n (csucc m)) *c aux. suff: A = (Bi n (csucc m)) *c (Yo (n <=c m) \1c (n -c m)). move => ->; congr (_ +c _); rewrite - cprodA; congr (_ *c _). by rewrite (cprodC (factorial m) _) - cprodA -(factorial_succ mN) cprodC. rewrite /A /Bi /aux - 2! cprodA; apply:f_equal; apply:f_equal. case: (p_or_not_p (n <=c m)) => le; Ytac0. rewrite (Nprod1r (NS_factorial (NS_diff (csucc m) nN))). by rewrite (cdiff_wrong (cleT le (cleS mN))) (cdiff_wrong le). case: (NleT_el nN mN) => // /(cleSltP mN) /(csucc_diff nN mN) s. rewrite s factorial_succ; fprops. move=> n m nN mN. rewrite -/(Bi n m); move: n nN m mN; apply: Nat_induction. move=> m mN. rewrite /Bi cdiff_0n factorial0 (Nprod1r (NS_factorial mN)). move: m mN; apply: Nat_induction. rewrite binom00 factorial0 (cprod1l CS1) Y_true; fprops. move=> p pN aux; Ytac h; first by move: (cleNgt h (succ_positive p)). by rewrite binom0Sm // cprod0l. move=> N NN rN; apply: Nat_induction. move: (NS_succ NN) => sN; move: (NS_factorial sN) (cle0n sN) => fN sp. by rewrite /Bi (binomSn0 NN)(cdiff_n0 sN)factorial0 !(Nprod1l fN) Y_true. move => p pN bN. rewrite (ba4 _ _ NN pN) (rN _ pN)(rN _ (NS_succ pN)) factorial_succ //. case: (NleT_el (NS_succ pN) NN) => c1. have lepN:=(cleT (cleS pN) c1). case: (p_or_not_p (N <=c p)) => h; first case:(cleNgt (cleT c1 h) (cltS pN)). rewrite (Y_true c1)(Y_true lepN)(Y_true (cleT c1 (cleS NN))) (Y_false h). by rewrite - cprodDr (Nsucc_rw pN) (Nsucc_rw NN) csumA (cdiff_rpr lepN). move /(cltSleP pN): (c1) => c2. rewrite (Y_false (cltNge c1)) cprod0l. case: (equal_or_not N p) => epN. rewrite - epN (Y_true (cleR (CS_nat NN))) csum0l ? Y_true; fprops. move:(cltNge (conj c2 epN)) => c3. move /(cleSSP (proj32 c2) (proj31 c2)): (c3) => c4. by Ytac0; Ytac0; rewrite cprod0l // (Nsum0l NS0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)