clear ih
case cons.intro
x : ChinesePair
xs : List ChinesePair
ih : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs → ∃ m, ∀ x ∈ xs, m ≡ x.remainder [MOD x.modulus]
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
case cons.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]