Inequalities.S
module P : Polynome.T with type t = p and type r = Shostak.Combine.r
module MINEQS : sig ... end
val current_age : unit -> Numbers.Z.t
val create_ineq : P.t -> P.t -> bool -> Expr.t option -> Explanation.t -> t
val print_inequation : Stdlib.Format.formatter -> t -> unit