仕事で a > c * n または b > c * m みたいな条件を判定する必要があり、 b / m > a / n の関係が成り立っているので b > c * m だけ確かめればいい、みたいなことを考えました。 ふと、本当にそうだっけ？と思ったので Lean4 で証明してみました。 variable…