# search [`x <= y / z`];;
val it : (string * thm) list =
[("RAT_LEMMA4",
|- &0 < y1 /\ &0 < y2 ==> (x1 / y1 <= x2 / y2 <=> x1 * y2 <= x2 * y1));
("REAL_LE_DIV", |- !x y. &0 <= x /\ &0 <= y ==> &0 <= x / y);
("REAL_LE_DIV2_EQ", |- !x y z. &0 < z ==> (x / z <= y / z <=> x <= y));
("REAL_LE_RDIV_EQ", |- !x y z. &0 < z ==> (x <= y / z <=> x * z <= y));
("SUM_BOUND_GEN",
|- !s t b.
FINITE s /\ ~(s = {}) /\ (!x. x IN s ==> f x <= b / &(CARD s))
==> sum s f <= b)]
Search for theorems whose name contains