proposition: Lemma b'_rec_eq (o : nat) (n := Posz o) : b'_rec o.+2 = - (annotated_recs_c.P_cf0 n * b'_rec o + annotated_recs_c.P_cf1 n * b'_rec o.+1) / annotated_recs_c.P_cf2 n.
proof: Proof. by []. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs