proposition: Theorem recAperyA (n : int) : 2 <= n :> int -> c.P_horner a n = 0.
proof: Proof. move=> nge2. rewrite /c.P_horner (punk.sound_telescoping P_eq_Delta_Q); last lia. set telQ := (X in X + _ + _). set onD := (X in _ + X + _). set remP := (X in _ + _ + X). have onDE : onD = c.P_horner (c ^~ n) n - (c.Q_flat c n (int.shift 1 n) - c.Q_flat c n n). rewrite /onD /c.not_D big_int_cond (eq_bigl (pred1 n)) => [|? /=]; last lia. by rewrite big_pred1_eqz ifT //; lia. have {telQ} -> : telQ + onD = c.P_horner (c ^~ n) n + c.Q_flat c n n. by rewrite onDE /telQ /c.Q_flat /c.Q_cf0_0 /int.shift /= /int.shift1; ring. rewrite {}/remP [bigop]unlock /= !add0r !addr0 -!int.shift2Z. rewrite /c.P_horner /c.P_seq /punk.horner_seqop /=. rewrite /c.Q_flat. have -> : int.shift1 n = int.shift 1 n by done. rewrite int.shift0 int.shiftS. rewrite (@c_Sk (int.shift 2 n) (int.shift 1 n)); last first. by rewrite /c.precond.Sk; lia. rewrite (@c_Sk (int.shift 2 n) n); last by rewrite /c.precond.Sk; lia. rewrite (@c_Sk (int.shift 1 n) n); last by rewrite /c.precond.Sk; lia. rewrite (@c_Sn (int.shift 1 n) n); last by rewrite /c.precond.Sn; lia. rewrite (@c_Sn n n); last by rewrite /c.precond.Sn; lia. set c1 := c _ _. Fail set c2 := c _ _. rewrite /c.Sn_cf0_0 /c.Sk_cf0_0 /c.P_cf0 /c.P_cf1 /c.P_cf2 /c.Q_flat /c.Q_cf0_0 !int.shift2R. by field; ring_lia. Qed.