chore(archive/imo): fix some naming inconsistencies and whitespace (#19155)

I realize that this is the third PR concerning namespacing the files in `archive/imo`.  These are some simple inconsistencies in naming.  There is no rush in merging this PR, but in the long run it might help to have consistent namespacing, so that batch renames can be simpler.

Author: adomani

archive/imo/imo1975_q1.lean

@@ -31,9 +31,7 @@ variables (hx : antitone_on x (finset.Icc 1 n))
 variables (hy : antitone_on y (finset.Icc 1 n))
 include hx hy hσ
 
-namespace imo1975_q1
-
-theorem IMO_1975_Q1 :
+theorem imo1975_q1 :
   ∑ i in finset.Icc 1 n, (x i - y i) ^ 2 ≤ ∑ i in finset.Icc 1 n, (x i - y (σ i)) ^ 2 :=
 begin
   simp only [sub_sq, finset.sum_add_distrib, finset.sum_sub_distrib],
@@ -48,5 +46,3 @@ begin
   -- them being `decreasing`
   exact antitone_on.monovary_on hx hy
 end
-
-end imo1975_q1

archive/imo/imo1977_q6.lean

@@ -36,6 +36,7 @@ begin
 end
 
 end imo1977_q6
+
 open imo1977_q6
 
 theorem imo1977_q6 (f : ℕ+ → ℕ+) (h : ∀ n, f (f n) < f (n + 1)) :

archive/imo/imo1988_q6.lean

@@ -186,6 +186,7 @@ begin
 end
 
 end imo1988_q6
+
 open imo1988_q6
 
 /--Question 6 of IMO1988. If a and b are two natural numbers

archive/imo/imo1994_q1.lean

@@ -46,6 +46,7 @@ begin
 end
 
 end imo1994_q1
+
 open imo1994_q1
 
 theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : finset ℕ) (hm : A.card = m + 1)

archive/imo/imo1998_q2.lean

@@ -198,6 +198,7 @@ lemma clear_denominators {a b k : ℕ} (ha : 0 < a) (hb : 0 < b) :
 by rw div_le_div_iff; norm_cast; simp [ha, hb]
 
 end imo1998_q2
+
 open imo1998_q2
 
 theorem imo1998_q2 [fintype J] [fintype C]

archive/imo/imo2001_q2.lean

@@ -67,6 +67,7 @@ calc _ ≥ _ : add_le_add (add_le_add (bound ha hb hc) (bound hb hc ha)) (bound
    ... = 1 : by rw [h₁, h₂, ← add_div, ← add_div, div_self $ ne_of_gt $ denom_pos ha hb hc]
 
 end imo2001_q2
+
 open imo2001_q2
 
 theorem imo2001_q2 (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :

archive/imo/imo2005_q3.lean

@@ -45,6 +45,7 @@ begin
 end
 
 end imo2005_q3
+
 open imo2005_q3
 
 theorem imo2005_q3 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x*y*z ≥ 1) :

archive/imo/imo2005_q4.lean

@@ -55,8 +55,12 @@ begin
   ... = 0 : by ring,
 end
 
+end imo2005_q4
+
+open imo2005_q4
+
 /-- Main statement:  The only positive integer coprime to all terms of the sequence `a` is `1`. -/
-example {k : ℕ} (hk : 0 < k) : (∀ n : ℕ, 1 ≤ n → is_coprime (a n) k) ↔ k = 1 :=
+theorem imo2005_q4 {k : ℕ} (hk : 0 < k) : (∀ n : ℕ, 1 ≤ n → is_coprime (a n) k) ↔ k = 1 :=
 begin
   split, rotate,
   { -- The property is clearly true for `k = 1`
@@ -95,5 +99,3 @@ begin
   -- Contradiction!
   contradiction,
 end
-
-end imo2005_q4

archive/imo/imo2006_q3.lean

@@ -136,6 +136,7 @@ begin
 end
 
 end imo2006_q3
+
 open imo2006_q3
 
 theorem imo2006_q3 (M : ℝ) :

archive/imo/imo2006_q5.lean

@@ -201,6 +201,7 @@ begin
 end
 
 end imo2006_q5
+
 open imo2006_q5
 
 /-- The general problem follows easily from the k = 2 case. -/