proposition: Lemma cleanup_R_correct: forall (e : Expr_R), interpret_R e = interpret_R (cleanup_R e).
proof: Proof. intros e; induction e as [q|r|z|f a IHa|f a IHa b IHb|a IHa b]. - cbn. destruct q as [n d]; destruct d; try reflexivity. unfold Q2R; cbn; ltac1:(lra). - reflexivity. - reflexivity. - cbn; rewrite IHa; reflexivity. - cbn; rewrite IHa, IHb; reflexivity. - cbn; rewrite IHa; reflexivity. Qed.
imports: Reals ZArith QArith Lra Lia Ltac2.Ltac2 Ltac2.Printf Ltac2.Bool