fact: Fixpoint b'_rec (n : nat) : rat := match n with | 0 => b 0 | 1 => b 1 | S (S o as o') => let n' := Posz o in - (annotated_recs_c.P_cf0 n' * b'_rec o + annotated_recs_c.P_cf1 n' * b'_rec o') / annotated_recs_c.P_cf2 n' end.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs