proposition: Lemma PEvalE l e : PEeval 0 1 +%R *%R (fun x y => x - y) -%R F_of_Z nat_of_N (@GRing.exp F) l e = PEeval 0 1 +%R *%R (fun x y => x - y) -%R (fun n => (int_of_Z n)%:~R) nat_of_N (@GRing.exp F) l e.
proof: Proof. elim: e => //= [| ? -> ? -> | ? -> ? -> | ? -> ? -> | ? -> | ? ->] //. by case=> [|[p|p|]|[p|p|]]; rewrite //= nmulrn; congr intmul; lia. Qed.
imports: elpi(elpi) Coq(ZArith Ring Ring_polynom Field_theory) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)