Докажите теорему об остатках в Китае, используя Coq
Я пытаюсь доказать китайскую теорему об остатках, используя Coq. Я уже доказал следующие леммы:
Lemma modulo_tran : forall a b c n : Z, (a == b [ n ]) -> (b == c [ n ]) -> (a == c [ n ]) .
Lemma modulo_plus_subst : forall a b c n : Z, (a == b [ n ]) -> (a + c == b + c [ n ]) .
Lemma modulo_mult_subst : forall a b c n : Z, (a == b [ n ]) -> (a * c == b * c [ n ]) .
И сейчас я пытаюсь доказать:
Hypothesis m n : Z .
Hypothesis co_prime : rel_prime m n .
Theorem modulo_inv : forall m n : Z, rel_prime m n -> exists x : Z, (m * x == 1 [ n ]) .
Я подумал, поскольку в начале теоремы есть "загадка", я должен ввести M и N в Coq. Получилось так:
1 subgoal
m, n : Z
co_prime : rel_prime m n
M, N : Z
______________________________________(1/1)
rel_prime M N -> exists x : Z, (M * x == 1 [N])
Тогда я не могу понять, что мне делать с гипотезой co_prime, чтобы доказать существование x, который встречается (M * x == 1 [N]). Я должен доказать это с упомянутыми леммами, верно? Может ли кто-нибудь помочь мне с этим?
Я впервые использую Coq, извините, если это звучало повсюду.
PS Определение по модулю дано ниже:
Definition modulo (a b n : Z) : Prop := (n | (a - b)) .
Notation "( a == b [ n ])" := (modulo a b n) .
Мое неофициальное доказательство (не уверен, помогло ли это):
let x_0 = mx + a = ny + b
[ x_0 = a (mod m)
[ y_0 = b (mod n)
[ x = a (mod m)
[ x = a (mod n)
[ x - x_0 = 0 (mod m)
[ x - x_0 = 0 (mod n)
x - x_0 = 0 (mod mn)
x = x_0 (mod mn)