kdrag.theories.real.arb.arb_lt_ax

kdrag.theories.real.arb.arb_lt_ax(lhs: ArithRef, rhs: ArithRef) → Proof

Use numerical evaluation to confirm ball of lhs is completely below ball of rhs

>>> arb_lt_ax(3.14, real.pi)
|- 157/50 < pi
Parameters:

  • lhs (ArithRef)

  • rhs (ArithRef)

Return type:

Proof