proposition: Lemma F9 n: (\sum_(i<n.+1) i ^ 5 ) * 12 = n * n * (n.+1) * (n.+1) * (2*n*n + 2*n -1).
proof: Proof. have pa: (120 * 12 = (48 * 5) *6) by done. have pb: (240 * 12 = (144 * 4) *5) by done. have pc: (150 * 12 = (150 * 3) *4) by done. have pd: (30 * 12 = (60 * 2) *3) by done. have pe: (12 = 2 * 6) by done. rewrite F9aux 4!mulnDl mulnAC pd (mulnAC 150) pc (mulnAC 240) pb. rewrite (mulnAC 120) pa {1} pe (mulnA _ 2) bin2' - (mulnA _ 3) - (mulnA _ 4). rewrite - (mulnA _ 5) - (mulnA _ 6) - 4! mul_bin_diag {pa pb pc pd pe}. rewrite (mulnCA (_ *5)) (mulnCA (_ * 4)) (mulnCA (_ * 3)) (mulnCA (60 * 2)). rewrite (mulnC n) - mulnA - 4! mulnDr (mulnAC n n) (mulnC n n.+1) - 7!mulnA. congr (_ * _); case:n => // n; rewrite - 4! mul_bin_diag. rewrite (mulnCA 60) (mulnCA 150) (mulnCA 144) (mulnCA 48) - 4! mulnDr. rewrite {2} (mulnSr 2 n) (addnA _ 1 1) addnA addnK -3 !addnA. have ->: (2 * n.+1 * n.+1 + (2 * n + 1)) = (2* n +6) *n +3. rewrite - mulnA mulnSr mulnDr mulnA mulnSr addnA addnAC - (addnA _ _ 1). by rewrite addnAC - mulnDl -2!addnA addnA - mulnDl -addnA. have ->: n.+1 * (n.+2 * ((2 * n + 6) * n + 3)) = 6 + n * (n.+1 * (n.+2) * (2*n +6) + 3* (n+3)). rewrite 3!mulnDr 3!mulnA mulnC addnCA (mulnCA _ 3) - (mulnDr 3 2). by rewrite (mulnC 3) {2} mulSn -{2} add2n -{2} addn2 -(addnA 2) -mulnS -addnS. congr (_ * (6 + _)); case:n => // n. have ->: n.+2 * n.+3 * (2 * n.+1 + 6) + 3 * (n.+1 + 3) = 60 + n * (2*n*n + 18 * n + 55 ). rewrite (addSn n 3) - addnS (mulnDr 3) addnA (mulnSr 2 n) -(addnA _ 2). rewrite mulnDr - {3} (addn2 n) mulnDl - {3} (addn3 n) (mulnDr 2). rewrite (mulnC 2) addnA - mulnDr mulnDl addnA mulnC - 2!mulnA. rewrite - mulnDr addnAC addnC -addnA addnA mulnC - mulnDr addnC. congr (60 + (n * _)); rewrite - (addn3 n) - addnA mulnDl (mulnC n 8). rewrite -(addn2 n) mulnA mulnDr (mulnAC 2 _ 3) (mulnDr 6) addnC. rewrite (addnA _ (6 * n)) -mulnDl mulnDr (addnCA _ _ 40) 2!addnA. by rewrite -2!mulnDl -3!addnA (addnCA 8) (mulnC 2). rewrite - (mulnA 75 2) - (mulnA 12 4) - (mulnA 48 3) - 3! mul_bin_diag bin1. rewrite mulnC (mulnCA 75) (mulnCA 48) (mulnCA 12) - 3! mulnDr. congr (_ * (60 + _)). case:n => // n; rewrite - (mulnA 24 2) - (mulnA 4 3) - 2! mul_bin_diag bin1. rewrite mulnCA (mulnCA 4) mulnC - 2!mulnDr; congr (_ * _). transitivity (75 +((22 + 2 * n) * n)). congr (_ + _); case:n => //n; rewrite - (mulnA 2 2) - mul_bin_diag !bin1. by rewrite (mulnC _ n) mulnA -mulnDl - (addnA 22 2) (mulnS 2 n). rewrite (mulnSr 18 n) - 2!addnA addnCA addnA 2! mulnSr (addnA (18 * n)). rewrite -mulnDl {1} (addnC _ 2) (addnA 18) (addnA _ _ 2) -mulnDl. by rewrite -addnA addnC addnAC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)