2019-12-12から1日間の記事一覧
問38 Midpoint https://top-prover.top/problem/38 Require Export Arith. Definition task := forall m n, S m < n -> m < (m + n) / 2 < n. まず初めに、Search _ inside Lt. SearchAbout "div" inside Nat. などで使えそうな定理を探す。 Phase 1, div2 x…
問38 Midpoint https://top-prover.top/problem/38 Require Export Arith. Definition task := forall m n, S m < n -> m < (m + n) / 2 < n. まず初めに、Search _ inside Lt. SearchAbout "div" inside Nat. などで使えそうな定理を探す。 Phase 1, div2 x…