proposition: Lemma recD1_flat (n k : int) : P1_flat s n k = P1_horner s n k.
proof: Proof. rewrite /P1_flat /d.P1_flat /P1_horner /d.P1_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 _ _. set s4 := s _ _. set s5 := s _ _. ring. Qed.
imports: annotated_recs_s