fact: Fixpoint cleanup_R (e : Expr_R) : Expr_R := match e with | ER_Q (z # 1) => ER_Z z | ER_Q (n # d) => ER_Binary EB_Div (ER_Z n) (ER_Z (Z.pos d)) | ER_R r => e | ER_Z z => e | ER_Unary f a => ER_Unary f (cleanup_R a) | ER_Binary f a b => ER_Binary f (cleanup_R a) (cleanup_R b) | ER_Pow a b => ER_Pow (cleanup_R a) b end.
imports: Reals ZArith QArith Lra Lia Ltac2.Ltac2 Ltac2.Printf Ltac2.Bool