fact: Fixpoint split_expr (e : expr) (lp lc : list expr) := match e with | Evar n => Scomposed lp lc | Econst o => Sconst | Eunary o e1 => match split_expr e1 lp lc with | Sconst => Sconst | Scomposed lp lc => Scomposed (cons_unique e lp) lc end | Ebinary o e1 e2 => match split_expr e2 lp lc with | Sconst => match split_expr e1 lp lc with | Sconst => Sconst | Scomposed lp lc => Scomposed (cons_unique e lp) (rcons_unique e2 lc) end | Scomposed lp lc => match split_expr e1 lp lc with | Sconst => Scomposed (cons_unique e lp) (rcons_unique e1 lc) | Scomposed lp lc => Scomposed (cons_unique e lp) lc end end end.
imports: Coq(ZArith Reals List Psatz) Xreal Tree