proposition: Lemma Fnorm_formula_correct k (ff : RFormula F) : Feval_formula k ff = Fnorm_formula k ff.
proof: Proof. case: ff => l o r /=; rewrite !Lra.Rnorm_correct addE oppE subE mulE expE. rewrite F_of_QE /R_of_Q/= mul0r mul1r invr1. by congr Feval_op2; apply: Lra.Rnorm_eq => invb n; rewrite mulr1; case: n => [|p|p] /=; rewrite ?(invr0, mul0r, mul1r)//; rewrite mulNr -divrN mul1r NegzE prednK ?nmulrn//; lia. Qed.
imports: elpi(elpi) Coq(QArith Ring) Coq.micromega(RingMicromega QMicromega EnvRing Tauto Lqa) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)