proposition: Lemma b'_Sn2_rew (n : int) : n >= 0 -> b' (int.shift 2 n) = - (annotated_recs_c.P_cf0 n * b' n + annotated_recs_c.P_cf1 n * b' (int.shift 1 n)) / annotated_recs_c.P_cf2 n.
proof: Proof. case: n => // o _. rewrite 2!int.shift2Z -2!PoszD. have -> : (o + 2)%N = o.+2 by rewrite addnC. have -> : (o + 1)%N = o.+1 by rewrite addnC. by rewrite b'_Posz b'_rec_eq. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs