proposition: Lemma b_Sn2_at_1 : annotated_recs_c.P_horner b 1 = 0.
proof: Proof. rewrite /annotated_recs_c.P_horner /punk.horner_seqop /=. rewrite initial_conds.b1_eq initial_conds.b2_eq initial_conds.b3_eq. rewrite /annotated_recs_c.P_cf0 /annotated_recs_c.P_cf1 /annotated_recs_c.P_cf2. by field; ring_lia. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs