proposition: Lemma Rnorm_correct (e : RExpr R') : Reval e = Rnorm id e.
proof: Proof. exact: Rnorm_correct_rec idfun _. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)