sig
  type t =
      Left of ArithLit.op * Z.t Monome.Focus.t * Z.t Monome.t
    | Right of ArithLit.op * Z.t Monome.t * Z.t Monome.Focus.t
    | Div of Z.t Monome.Focus.t ArithLit.divides
  val mk_left :
    ArithLit.op -> Z.t Monome.Focus.t -> Z.t Monome.t -> ArithLit.Focus.t
  val mk_right :
    ArithLit.op -> Z.t Monome.t -> Z.t Monome.Focus.t -> ArithLit.Focus.t
  val mk_div :
    ?sign:bool -> Z.t -> power:int -> Z.t Monome.Focus.t -> ArithLit.Focus.t
  val get :
    ArithLit.lit -> Libzipperposition.Position.t -> ArithLit.Focus.t option
  val get_exn :
    ArithLit.lit -> Libzipperposition.Position.t -> ArithLit.Focus.t
  val focus_term : ArithLit.lit -> ArithLit.term -> ArithLit.Focus.t option
  val focus_term_exn : ArithLit.lit -> ArithLit.term -> ArithLit.Focus.t
  val replace : ArithLit.Focus.t -> Z.t Monome.t -> ArithLit.lit
  val term : ArithLit.Focus.t -> ArithLit.term
  val focused_monome : ArithLit.Focus.t -> Z.t Monome.Focus.t
  val opposite_monome : ArithLit.Focus.t -> Z.t Monome.t option
  val opposite_monome_exn : ArithLit.Focus.t -> Z.t Monome.t
  val is_max : ord:Libzipperposition.Ordering.t -> ArithLit.Focus.t -> bool
  val is_strictly_max :
    ord:Libzipperposition.Ordering.t -> ArithLit.Focus.t -> bool
  val map_lit :
    f_m:(Z.t Monome.t -> Z.t Monome.t) ->
    f_mf:(Z.t Monome.Focus.t -> Z.t Monome.Focus.t) ->
    ArithLit.Focus.t -> ArithLit.Focus.t
  val product : ArithLit.Focus.t -> Z.t -> ArithLit.Focus.t
  val scale :
    ArithLit.Focus.t ->
    ArithLit.Focus.t -> ArithLit.Focus.t * ArithLit.Focus.t
  val scale_power : ArithLit.Focus.t -> int -> ArithLit.Focus.t
  val apply_subst :
    renaming:Libzipperposition.Substs.Renaming.t ->
    Libzipperposition.Substs.t ->
    ArithLit.Focus.t Libzipperposition.Scoped.t -> ArithLit.Focus.t
  val apply_subst_no_renaming :
    Libzipperposition.Substs.t ->
    ArithLit.Focus.t Libzipperposition.Scoped.t -> ArithLit.Focus.t
  val unify :
    ?subst:Libzipperposition.Substs.t ->
    ArithLit.Focus.t Libzipperposition.Scoped.t ->
    ArithLit.Focus.t Libzipperposition.Scoped.t ->
    (ArithLit.Focus.t * ArithLit.Focus.t * Libzipperposition.Substs.t)
    Sequence.t
  val fold_terms :
    ?pos:Libzipperposition.Position.t ->
    ArithLit.lit ->
    (ArithLit.Focus.t * Libzipperposition.Position.t) Sequence.t
  val op : ArithLit.Focus.t -> [ `Binary of ArithLit.op | `Divides ]
  val unfocus : ArithLit.Focus.t -> ArithLit.lit
  val pp : ArithLit.Focus.t CCFormat.printer
  val to_string : ArithLit.Focus.t -> string
end