Как доказать, что деление является отменяющим?

Question

Я хочу доказать, что (c * a) / (c * b) = a / b в Агде, используя функцию деления, определенную в стандартной библиотеке. Доказательства продолжают возвращаться к этой вещи div-helper, с которой очень трудно работать, и рассуждают.

open import Data.Nat.DivMod using (_/_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Nat using (ℕ; suc; zero)

/-cancelˡ : ∀ c a b {b≢0} {b*c≢0} → ((c * a) / (c * b)) {b*c≢0} ≡ (a / b) {b≢0}
/-cancelˡ (suc c) a (suc b) {b≢0} {b*c≢0} = ?

Эта дыра упрощается до:

div-helper 0 (b + c * suc b) (a + c * a) (b + c * suc b) ≡ div-helper 0 b a b

Answer 1

Обратите внимание, что инварианты div-helper с уважением прописаны во встроенном файле Agda.Builtin.Nat. Вы должны изложить более общую версию своей леммы, удовлетворяющую div-helper.