Function product_less_than_known 

pub(crate) fn product_less_than_known(
    left_a: &Expr,
    left_b: &Expr,
    right_a: &Expr,
    right_b: &Expr,
    less_than: &BTreeSet<(Expr, Expr)>,
    positive: &BTreeSet<Expr>,
) -> bool

Returns whether known facts imply left_a * left_b < right_a * right_b.