let of_mono q x = if Q.is_zero q then mk_zero else if Q.is_one q then x else match x with | App(Arith(Num(p)), []) -> mk_num (Q.mult q p) | _ -> mk_app (multq q) [x]