proposition: Lemma recD4_flat (n k : int) : P4_flat s n k = P4_horner s n k.
proof: Proof. rewrite /P4_flat /d.P4_flat /P4_horner /d.P4_horner. rewrite /punk.biv_horner_seqop2 /punk.biv_horner_seqop. rewrite /punk.biv_horner_seqop_rec /=. set s1 := s _ _. set s2 := s _ _. set s3 := s _ _. ring. Qed.
imports: annotated_recs_s