Fix the Rocq statements of 1962 A2, A6 and B5 (#358)

coq/src/putnam_1962_a2.v

@@ -11,7 +11,12 @@ Local Open Scope classical_set_scope.
 
 Variable R : realType.
 Definition mu := [the measure _ _ of @lebesgue_measure R].
-Definition putnam_1962_a2_solution : set (R -> R) := [set f | exists a c : R, a >= 0 /\ f = (fun x : R => a / (1 - c * x) ^ 2)].
+Definition putnam_1962_a2_solution : set (R -> R) := [set f |
+     (exists a c : R, a >= 0 /\ f = (fun x : R => a / (1 - c * x) ^ 2))
+  \/ (exists a c : R, a >= 0 /\ 0 < c /\ f = (fun x : R => if x < 1 / c then a / (1 - c * x) ^ 2 else 0))
+  \/ ((forall x, f x >= 0) /\ forall x : R, 0 < x -> f x = 0)
+  \/ (exists e : R, 0 < e /\ f 0 = 0 /\ (forall x, f x >= 0) /\
+        forall x : R, 0 < x < e -> \int[mu]_(t in [set t | 0 <= t <= x]) f t = 0)].
 Theorem putnam_1962_a2
     (P : (set R) -> (R -> R) -> Prop)
     (P_def : forall s f, P s f <-> ((forall x, f x >= 0) /\ forall x, x \in s -> 

coq/src/putnam_1962_a6.v

@@ -3,6 +3,6 @@ Theorem putnam_1962_a6
     (A : Ensemble Q)
     (hSSadd : forall a b : Q, (A a /\ A b) -> A (a + b))
     (hSSprod : forall a b : Q, (A a /\ A b) -> A (a * b))
-    (hSScond : forall r : Q, (A r \/ A (-r) \/ r = 0) /\ ~(A r \/ A (-r)) /\ ~(A r /\ r = 0) /\ ~(A (-r) /\ r = 0))
+    (hSScond : forall r : Q, (A r \/ A (-r) \/ r == 0) /\ ~(A r /\ A (-r)) /\ ~(A r /\ r == 0) /\ ~(A (-r) /\ r == 0))
     : A = (fun r : Q => r > 0).
 Proof. Admitted.

coq/src/putnam_1962_b5.v

@@ -12,5 +12,5 @@ Theorem putnam_1962_b5
     (n : nat)
     (ng1 : gt n 1)
     (sumf : nat -> R := fun N => \sum_(1 <= i < N.+1) ((i%:R / N%:R) ^+ N))
-    : (3 * (n%:R + 1) + 1) / (2 * n%:R + 2) < sumf n < 2.
+    : (3 * n%:R + 1) / (2 * n%:R + 2) < sumf n < 2.
 Proof. Admitted.