-
Notifications
You must be signed in to change notification settings - Fork 0
/
Solution.v
44 lines (39 loc) · 1.04 KB
/
Solution.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
Require Import Problem ZArith ZArith.Znumtheory.
Theorem solution : task.
Proof.
unfold task.
intros.
unfold Square; unfold Square in H2.
remember (Z.sqrt (n * m)) as k.
remember (Z.gcd k m) as x.
remember (Z.gcd k n) as y.
apply (proj2 (Zgcd_1_rel_prime n m)) in H1.
assert (y * k = n * x).
subst x y.
rewrite <- Z.gcd_mul_mono_l_nonneg; [|omega].
rewrite <- Z.gcd_mul_mono_r_nonneg; [|subst k; apply Z.sqrt_nonneg].
rewrite H2.
rewrite Z.gcd_comm.
auto.
assert (Z.gcd x y = 1).
subst x y.
rewrite <- Z.gcd_assoc.
rewrite (Z.gcd_comm m).
rewrite <- Z.gcd_assoc.
rewrite H1.
repeat rewrite Z.gcd_1_r.
auto.
assert (n = y * Z.gcd k n).
rewrite <- Z.gcd_mul_mono_l_nonneg; [|subst y; apply Z.gcd_nonneg].
rewrite H3; clear H3.
rewrite Z.mul_comm.
rewrite Z.gcd_mul_mono_r_nonneg; [|omega].
rewrite H4; clear H4.
omega.
rewrite <- Heqy in H5.
replace (Z.sqrt n) with y; [auto|].
specialize (Z.gcd_nonneg k n); intro.
rewrite <- Heqy in H6.
rewrite <- (Z.sqrt_square y H6).
subst n; auto.
Qed.