proposition: Lemma b'2_eq : b' 2%N = rat_of_Z 351 / rat_of_Z 4.
proof: Proof. rewrite -[Posz 2]/(int.shift 2 0) b'_Sn2_rew // b'0_eq b'1_eq. rewrite /annotated_recs_c.P_cf0 /annotated_recs_c.P_cf1 /annotated_recs_c.P_cf2. by apply/eqP; rewrite rat_of_ZEdef; vm_compute. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs