proposition: Lemma Qeval_expr_compat : forall env e, Qeval_expr env e = Qeval_expr' env e.
proof: Proof. induction e ; simpl ; subst ; try congruence. - reflexivity. - rewrite IHe. apply QNpower. Qed.
imports: OrderedRing RingMicromega Refl QArith Qfield EnvRing