proposition: Theorem P2_eq_Delta_Q2 : d.CT2 d.
proof: Proof. move=> n m k; rewrite /d.not_D2 => ?. rewrite /d.P2_horner /d.P2_seq. rewrite /punk.biv_horner_seqop2 /punk.biv_horner_seqop. rewrite /punk.biv_horner_seqop_rec /punk.pfun2 /d.Q2_flat /=. do 6! (rewrite d_Sn; last by rewrite /d.precond.Sn; lia). rewrite d_Sm; last by rewrite /d.precond.Sm; lia. set d_nmk := d _ _ _. Fail set dtest := d _ _ _. rewrite /d.P2_cf0_0 /d.P2_cf1_0 /d.P2_cf2_0 /d.P2_cf3_0 /d.Q2_cf0_0_0 /d.Q2_cf1_0_0 /d.Q2_cf2_0_0 /d.Sk_cf0_0_0 /d.Sm_cf0_0_0 /d.Sn_cf0_0_0. rewrite !int.shift2R. by field; ring_lia. Qed.
imports: annotated_recs_s