proposition: Lemma sum_sum4 n : (n ^ 3).*2 = 6 * (\sum_(0 <= i < n) i ^ 2) + 3 * n * n.-1 + n.*2.
proof: Proof. rewrite sum_consecutive_cube -sum_sum3 -mul2n sum_mull. apply: eq_big_nat => i Hi. by rewrite succ_cube addKn 2!mulnDr !mulnA. Qed.
imports: mathcomp(all_ssreflect)