proposition: Fact lt_0_Dz3seq (i j : nat) : (j < i)%N -> 0 < z3seq i - z3seq j.
proof: Proof. move=> ltji; rewrite Dz3seqE; last exact: ltnW. rewrite big_nat_recr //=; apply: ltr_wpDl; last first. by rewrite invr_gt0 exprn_gt0 // ltr0n; apply: leq_trans ltji. by apply: sumr_ge0 => *; rewrite invr_ge0 exprn_ge0 // ler0n. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics bigopz harmonic_numbers seq_defs