proposition: Lemma F8 n: (\sum_(i<n.+1) i ^ 4 ) * 30 = n * (n.+1) * (n.*2.+1) * (3*n*n + 3*n -1).
proof: Proof. have pa: (24 * 30 = (36 * 4) *5) by done. have pb: (36 * 30 = (90 * 3) *4) by done. have pc: (14 * 30 = (70 * 2) *3) by done. have pd: (30 = 2 * 15) by done. rewrite F8aux 3! mulnDl mulnAC pc (mulnAC 36) pb (mulnAC 24) pa {1} pd. rewrite - (mulnA _ 3) - (mulnA _ 4) - (mulnA _ 5) - 3! mul_bin_diag /=. rewrite (mulnCA (_ *4)) (mulnCA (90 * 3)) (mulnCA (70 * 2)) (mulnA _ 2) bin2'. rewrite (mulnC n) - mulnA - 3! mulnDr -5!mulnA; congr (_ * _); case:n => //n. rewrite - 3! mul_bin_diag (mulnCA 70) (mulnCA 90) (mulnCA 36) - 3! mulnDr. congr (_ * _); case:n => // n. rewrite bin1 (_: 90 = 45 *2) // [in 36 * _] (_: 36 = (6 * 2) * 3) //. rewrite - (mulnA _ 2) - (mulnA _ 3) - 2! mul_bin_diag /= bin1 (mulnCA (6 * 2)). case:n => // n;rewrite - (mulnA 6) -mul_bin_diag /= bin1 mulnCA -addnA -mulnDr. rewrite (mulnC _ n) (mulnA 6) - mulnDl mulnCA. rewrite -(addnA 24) (addnC 21) (mulnAC 2 3) - (mulnDl (2 * n) 7 3). rewrite mulnDl addnA (mulnC n.+2) (mulnA 24) - (addnA 15) - mulnDl. rewrite (mulnS 24) addnA -(addnA 10 84) (mulnAC 2 12) (addnC 84). rewrite - (mulnDl (2 * n) 7) mulnDl addnA (addnC 15) 2!mulnSr. rewrite (mulnAC 2 5) - (addnA _ _ 15) - (addnA _ 10) - (mulnDl (2 * n) 7 5). rewrite - mulnA - mulnA - 2! mulnDr; congr (_ * _). by rewrite addnS - mul2n 3!mulnSr - 2!addnA //. rewrite {2} (mulnSr 3) addnA (addnS _ 2) subn1 (succnK) -mulnA - addnA. rewrite - (addnA 2 (3 * 1)) - (mulnA 3 4) - 3!mulnDr addnC. rewrite (mulnDl 2 2) - addnA -mulnDl add2n mul2n -addnn addnA addnCA. by rewrite add1n -addnA - mulnS (addnC _ n.+2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)