proposition: Fact Dz3seqE (i j : nat) : (j <= i)%N -> z3seq i - z3seq j = \sum_(j.+1 <= k < i.+1) (k%:Q ^ 3)^-1.
proof: Proof. rewrite -ltnS => leji; rewrite !z3seqE (big_cat_nat _ _ _ _ leji) //=. by rewrite addrAC addrN add0r. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics bigopz harmonic_numbers seq_defs