proposition: Lemma cleanup_simplify_R_correct: forall (e : Expr_R), interpret_R e = interpret_R (cleanup_R (simplify_R e)).
proof: Proof. intros e. rewrite <- cleanup_R_correct. apply simplify_R_correct. Qed.
imports: Reals ZArith QArith Lra Lia Ltac2.Ltac2 Ltac2.Printf Ltac2.Bool