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