proposition: Lemma Rnorm_formula_correct k (ff : RFormula R) : Reval_formula k ff = Rnorm_formula k ff.
proof: Proof. case: ff => l o r /=. by rewrite !Ring.Rnorm_correct R_of_ZE addE oppE subE mulE expE. 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)