proposition: Lemma F8_aux n: n ^ 4 = 24 * 'C(n, 4) + 36 * 'C(n, 3) + 14 * 'C(n, 2) + 'C(n, 1).
proof: Proof. elim:n => //n Hrec; rewrite - {1} addn1 Pascal 5! big_ord_recr big_ord0 /=. rewrite !exp1n expn0 expn1 !muln1 add0n /subn /= bin0 bin1 mul1n Hrec. rewrite !(binS n) 3! mulnDr bin0 addnA;congr (_ + 1). set a := 24 * 'C(n, 4); set b := 36 * 'C(n, 3). rewrite - 5! addnA -(addnA (a + _)) (addnAC a) - (addnA b). rewrite (addnCA ( 36 * 'C(n, 2))) - 4! addnA; congr (_ + (_ + (_ + _))). rewrite (_: 'C(4, 2) = 6) // (_: 'C(4, 3) = 4) // F7_aux bin1. rewrite (addnC _ (_ + n)) (addnC (24 * _)) - (addnA n); congr (n + _). rewrite - addnA mulnDr mulnA - addnA; congr (_ + _). rewrite F6_aux 2! mulnDr 2! mulnA bin1 - (addnA _ _ (4 * n)) - mulnDl. by rewrite addnAC addnA - mulnDl - addnA - mulnDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)