proposition: Theorem P3_eq_Delta_Q3 : d.CT3 d.
proof: Proof. move => n m k; rewrite /d.not_D3 => ?. rewrite /d.P3_horner /d.P3_seq /punk.biv_horner_seqop2 /punk.biv_horner_seqop. rewrite /punk.biv_horner_seqop_rec /punk.pfun2 /d.Q3_flat /=. do 2! (rewrite d_Sn; last by rewrite /d.precond.Sn; lia). rewrite d_Sk //. rewrite d_Sm; last by rewrite /d.precond.Sm; lia. set d_nmk := d _ _ _. Fail set dtest := d _ _ _. rewrite /d.P3_cf0_0 /d.P3_cf0_1 /d.P3_cf1_0 /d.P3_cf1_1 /d.Q3_cf0_0_0 /d.Sk_cf0_0_0 /d.Sm_cf0_0_0 /d.Sn_cf0_0_0. by field; ring_lia. Qed.
imports: annotated_recs_s