proposition: Lemma a_Sn2 (n : int) : 2 <= n :> int -> annotated_recs_c.P_horner a n = 0.
proof: Proof. by move=> h; exact: (ops_for_a.recAperyA c_ann h). Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics shift binomialz rat_of_Z seq_defs