proposition: Lemma z_Sn2 : annotated_recs_z.Sn2 ghn3.
proof: Proof. rewrite /annotated_recs_z.Sn2 /annotated_recs_z.precond.Sn2 => n ?. rewrite /ghn3 harmonic_numbers.ghn_Sn2 -/ghn3; last lia. rewrite /annotated_recs_z.Sn2_cf0 /annotated_recs_z.Sn2_cf1. by field; ring_lia. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics shift binomialz rat_of_Z seq_defs