proposition: Lemma b'_Sn4 (n : int) : n >= 0 -> annotated_recs_v.P_horner b' n = 0.
proof: Proof. move=> ?. rewrite /annotated_recs_v.P_horner /punk.horner_seqop [LHS]/=. rewrite !b'_Sn2_rew //; [ | lia ..]. set b'1 := b' _. set b'2 := b' _. Fail set b'3 := b' _. rewrite /annotated_recs_c.P_cf0 /annotated_recs_c.P_cf1 /annotated_recs_c.P_cf2. rewrite /annotated_recs_v.P_cf0 /annotated_recs_v.P_cf1. rewrite /annotated_recs_v.P_cf2 /annotated_recs_v.P_cf3 /annotated_recs_v.P_cf4. rewrite !rmorphD /=. field; ring_lia. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs