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