proposition: Lemma b'_eq_b (n : int) : n >= Posz 2 -> b' n = b n.
proof: Proof. apply: b'_eq_b_reduction => //. - by rewrite b'2_eq initial_conds.b2_eq. - by rewrite b'3_eq initial_conds.b3_eq. - rewrite -[(2 : int) + (2 : int)]/(int.shift 2 2). rewrite b'_Sn2_rew // b'2_eq b'3_eq. rewrite /annotated_recs_c.P_cf0 /annotated_recs_c.P_cf1. rewrite /annotated_recs_c.P_cf2. by initial_conds.solve_b_evaluation. - rewrite -[(2 : int) + (3 : int)]/(int.shift 2 3). rewrite b'_Sn2_rew // b'3_eq b'4_eq. rewrite /annotated_recs_c.P_cf0 /annotated_recs_c.P_cf1. rewrite /annotated_recs_c.P_cf2. by initial_conds.solve_b_evaluation. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs