1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14

def gcd(a b : Nat) : Nat :=
  if b > 0 then gcd b (a % b) else a
termination_by b
decreasing_by
  rename_i h
  exact Nat.mod_lt a h

#eval "test"

def N := 1000

def A := List.range N

#eval (A.map λ x => (A.map λ y => gcd x y).sum).sum