kdrag.theories.real.arb.arb_le_ax

kdrag.theories.real.arb.arb_le_ax(lhs0: ArithRef, rhs: ArithRef) → Proof
>>> arb_le_ax(3.14, real.pi)
|- 157/50 <= pi
>>> arb_le_ax(1,1)
|- 1 <= 1
Parameters:

  • lhs0 (ArithRef)

  • rhs (ArithRef)

Return type:

Proof