proposition: Theorem P_eq_Delta_Q : v.CT v.
proof: Proof. rewrite /v.CT => n k; rewrite /v.not_D => notD. rewrite /v.P_horner /v.P_seq /punk.horner_seqop /= /v.Q_flat. do 5! (rewrite v_Sn2; last by rewrite /v.precond.Sn2; lia). rewrite v_SnSk; last by rewrite /v.precond.SnSk; lia. rewrite v_Sk2; last by rewrite /v.precond.Sk2; lia. set v1 := v _ _; set v2 := v _ _; set v3 := v _ _. rewrite /v.P_cf0 /v.P_cf1 /v.P_cf2 /v.P_cf3 /v.P_cf4 /v.Sk2_cf0_0 /v.Sk2_cf0_1 /v.Sn2_cf0_0 /v.Sn2_cf1_0 /v.Sn2_cf0_1 /v.SnSk_cf0_0 /v.SnSk_cf1_0 /v.SnSk_cf0_1 /v.Q_cf0_0 /v.Q_cf1_0 /v.Q_cf0_1 . rewrite !int.shift2R. by field; ring_lia. Qed.