proposition: Lemma b_Sn2_almost (n : int) : n >= 2 :> int -> annotated_recs_c.P_horner b n = 0.
proof: Proof. move=> h. rewrite /annotated_recs_c.P_horner/punk.horner_seqop [LHS]/=. rewrite -!b'_eq_b; [ | lia ..]. have h' : 0 <= n by lia. rewrite b'_Sn2_rew //. field. by apply/expfz_neq0; ring_lia. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs