Theoremsmul_congr, mul_congr_left, mul_congr_right, mul, mul_pos, P24, P3_of_lt_of_lt, numeric_P1, numeric_P24, numeric_closed, P1_of_eq, P1_of_ih, P1_of_lt, P24_neg_left, P24_neg_right, P24_of_ih, P2_neg_left, P2_neg_right, trans, P3_comm, P3_neg, P3_of_ih, P3_of_le_left, P3_of_lt, P4_neg_left, P4_neg_right, argsRel_wf, ih1, ih1_neg_left, ih1_neg_right, ih1_swap, ih24_neg, ih3_of_ih, ih4, ih4_neg, ih₁₂, ih₂₁, main, mulOption_lt, mulOption_lt_iff_P1, mulOption_lt_mul_iff_P3, mulOption_lt_mul_of_equiv, mulOption_lt_of_lt, mulOptionsLTMul_of_numeric, mul_right_le_of_equiv, numeric_mul_option, numeric_of_ih, numeric_option_mul, numeric_option_mul_option, instIsStrictOrderedRing, instNontrivial, instZeroLEOneClass | 52 |