proposition: Lemma Qeval_expr_simpl : forall env e, Qeval_expr env e = match e with | PEc c => c | PEX j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) | PEopp pe1 => - (Qeval_expr env pe1) | PEpow pe1 n => Qpower (Qeval_expr env pe1) (Z.of_N n) end.
proof: Proof. destruct e ; reflexivity. Qed.
imports: OrderedRing RingMicromega Refl QArith Qfield EnvRing