proposition: Lemma ghn_Sn2 m (n_ : int) (n := n_%:Q) : n_ + 1 != 0 -> ghn m (int.shift 2 n_) = ((n + 1) ^ m / (n + 2%:Q) ^ m + 1) * ghn m (int.shift 1 n_) - (n + 1) ^ m / (n + 2%:Q) ^ m * ghn m n_.
proof: Proof. move=> pn2. case: (leP n_ 0) => hn. rewrite [in X in _ = _ - X]ghn_small // mulr0 subr0. rewrite {}/n; case: n_ pn2 hn => [ [] // _ _ | n hn2]. rewrite -[int.shift 2 0]/(int.shift 1 (int.shift 1 0)) [LHS]ghn_Sn_inhom //. by rewrite !int.shift2Z !add0r exp1rz mulrDl !mul1r addrC ghn1 mulr1. case: n hn2 => [| n] hn //. by rewrite !ghn_small ?mulr0 // NegzE int.shift2Z addrC !subzSS add0r oppr_le0. rewrite ?ghn_Sn_inhom ?ltW ?addr_gt0 //=. rewrite int.shift2R -/n. move: (ghn m n_) => x. apply/eqP; rewrite -subr_eq0 -!addrA addr_eq0; apply/eqP. elim: m => [|m ->]; first by field => //. rewrite !exprSz. by field; rewrite /= !expfz_eq0; ring_lia. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics shift bigopz