proposition: Lemma ghn_Sn_inhom m n : n >= 0 -> ghn m (int.shift 1 n) = ghn m n + ((n%:Q + 1)^m)^-1.
proof: Proof. move=> pn. by rewrite /ghn int.shift2Z big_int_recr /= ?rmorphD //= -lerBlDr. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics shift bigopz