proposition: Lemma cleanup_simplify_correct: forall (e : Expr_R), interpret_R e = interpret_R (cleanup (simplify e)).
proof: Proof. intros e. rewrite <- cleanup_correct. apply simplify_correct. Qed.
imports: Reals ZArith QArith Lra Lia