proposition: Lemma b'3_eq : b' 3%N = rat_of_Z 62531 / rat_of_Z 36.
proof: Proof. rewrite -[Posz 3]/(int.shift 2 1) b'_Sn2_rew // b'1_eq b'2_eq. rewrite /annotated_recs_c.P_cf0 /annotated_recs_c.P_cf1 /annotated_recs_c.P_cf2. by field. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs