proposition: Theorem recD3 (n k : int) : 0 <= k -> k < n -> P3_horner s n k = 0.
proof: Proof. move=> ? ?. rewrite /P3_horner /d.P3_horner. rewrite (punk.biv_sound_telescoping P3_eq_Delta_Q3); last by rewrite lerDr. set telQ := (X in X + _ + _). set onD := (X in _ + X + _). set remP := (X in _ + _ + X). rewrite [bigop]unlock /= !add0r !addr0 in remP *. rewrite_modulo_d_ann remP. rewrite {}/telQ /d.Q3_flat. set telQ := (X in X + _ + _). rewrite_modulo_d_ann telQ. have -> : onD = 0. rewrite /onD {remP telQ}. set F := BIG_F. clearbody F. rewrite big_int_cond /=. apply: big_pred0 => i. rewrite /d.not_D3. lia. rewrite {}/telQ {}/remP. rewrite !addr0. set d1 := d _ _ _. set d2 := d _ _ _. rewrite /d.P3_cf0_1 /d.P3_cf1_1 /d.Q3_cf0_0_0 /d.Sn_cf0_0_0 /d.Sk_cf0_0_0 /d.Sm_cf0_0_0. rewrite !int.shift2R. by field; ring_lia. Qed.
imports: annotated_recs_s