proposition: Lemma PCondP l le : reflect (PCond' True not and 0 1 +%R *%R (fun x y : F => x - y) -%R eq (fun n0 : Z => (int_of_Z n0)%:~R) nat_of_N (@GRing.exp F) l le) (PCond' true negb andb 0 1 +%R *%R (fun x y : F => x - y) -%R eq_op F_of_Z nat_of_N (@GRing.exp F) l le).
proof: Proof. elim: le => [/=|e1 /= [|e2 le] IH]. - exact: ReflectT. - by rewrite PEvalE; apply: (iffP negP); apply/contra_not => /eqP. - by rewrite PEvalE; apply: (iffP andP) => -[/eqP ? /IH ?]. 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)