use 0
case nil
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) []
⊢ ∃ m, ∀ x ∈ [], m ≡ x.remainder [MOD x.modulus]
case h
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) []
⊢ ∀ x ∈ [], 0 ≡ x.remainder [MOD x.modulus]