ふとした時の検証

仕事で

a > c * n または b > c * m

みたいな条件を判定する必要があり、

b / m > a / n

の関係が成り立っているので

b > c * m

だけ確かめればいい、みたいなことを考えました。

ふと、本当にそうだっけ？と思ったので Lean4 で証明してみました。

variable (p q: Prop)

example : (p ∨ q) ∧ (p → q) ↔ q := Iff.intro
  (fun ⟨h1, h2⟩ => h1.elim (fun h3 => h2 h3) (fun h3 => h3))
  (fun h => And.intro (Or.inr h) (fun _hp => h))

感想

だいぶ忘れている。