proposition: Theorem P_eq_Delta_Q (n k : int) : not_D n k -> P_horner (u ^~ k) n = Q_flat u n (int.shift 1 k) - Q_flat u n k.
proof: Proof. rewrite /not_D; andb_to_and => notD. rewrite /P_horner /P_seq /punk.horner_seqop /= /Q_flat. do 2! (rewrite u_Sn; last by rewrite /precond_Sn; intlia). rewrite u_Sk; last by rewrite /precond_Sk; intlia. rewrite /P_cf0 /P_cf1 /P_cf2 /Q_cf0_0 /Sn_cf0_0 /Sk_cf0_0. rewrite !int.shift2R. rat_field. by goal_to_lia; intlia. Qed.