Description

HOMEWORK 4
Please use the Coq file hw2-2.v to show the following instance of the Chinese remainder theorem:
Theorem 1. Let m,n ∈ Z and m,n be relatively prime. For every a,b ∈Z, there is an x ∈Z such that
x ≡ a (m) x ≡ b (n).
Hints:
• Bezout’s coefficients in the Coq standard library Znumtheory will be useful.
• A useful on-line information is Software Foundations .
• Another useful on-line information is Certified Programming with Dependent Types .
• Send me emails if you have any question.
1