proposition: Lemma z3seq_smd_maj (k : nat) : 0 < k%:Q -> (k.+1%:Q ^ 3)^-1 <= - 2%:Q^-1 * ((k.+1%:Q ^ 2) ^-1 - (k%:Q ^ 2) ^-1).
proof: Proof. move=> hr; set r := k.+1%:Q. have hkr : k%:Q = r - 1 by rewrite /r -addn1 PoszD rmorphD addrK. have hrk : r = k%:Q + 1 by rewrite hkr addrK. have lt1r : 1 < r by rewrite hrk ltrDr. rewrite hkr; set rhs := (X in _ <= X). have {rhs} -> : rhs = 2%:Q^-1 * (2%:Q * r - 1) / (r - 1) ^ 2 * (r ^ 2)^-1. by rewrite /rhs; field; ring_lia. have -> : (r ^ 3)^-1 = r ^-1 * (r ^ 2)^-1 by field; ring_lia. have le0r : 0 <= r by apply: ltW; apply: lt_trans lt1r. apply: ler_pM; rewrite ?invr_ge0 ?exprn_ge0 //. rewrite ler_pdivlMr; last first. by apply: exprz_gt0; rewrite subr_gt0. rewrite ler_pdivrMl; last by apply: lt_trans lt1r. rewrite -subr_ge0; set rhs := (X in _ <= X). have {rhs} -> : rhs = 3%:Q / 2%:Q * r - 1 by rewrite /rhs; field. by rewrite subr_ge0; apply/mulr_ege1/ltW. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics bigopz harmonic_numbers seq_defs