constructor
case h
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ x % b < b ∧ a * (x % b) ≡ c [MOD b]
case h.left
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ x % b < b

case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ a * (x % b) ≡ c [MOD b]