coq 1981-82 fixes

coq/src/putnam_1981_a1.v

@@ -1,12 +1,7 @@
-Require Import Nat Reals Coquelicot.Coquelicot. From mathcomp Require Import div.
-Definition putnam_1981_a1_solution := 1 / 8.
+Require Import Nat Reals Coquelicot.Coquelicot. From mathcomp Require Import div bigop.
+Definition putnam_1981_a1_solution : R := Rdiv 1 8.
 Theorem putnam_1981_a1
-    (prod_n : (nat -> nat) -> nat -> nat := fix prod_n (m: nat -> nat) (n : nat) :=
-        match n with
-        | O => m 0%nat
-        | S n' => mul (m n') (prod_n m n')
-    end)
-    (P : nat -> nat -> Prop := fun n k => 5 ^ k %| prod_n (fun m => Nat.pow m m) (S n) = true)
+    (P : nat -> nat -> Prop := fun n k => 5 ^ k %| (\prod_(1<=i<n+1) (i^i)) = true)
     (f : nat -> nat)
     (hf : forall (n: nat), gt n 1 -> P n (f n) /\ forall (k: nat), P n k -> le k (f n))
     : Lim_seq (fun n => INR (f n) / INR n ^ 2) = putnam_1981_a1_solution.

coq/src/putnam_1981_a3.v

@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_1981_a3_solution := 14.
+Definition putnam_1981_a3_solution := False.
 Theorem putnam_1981_a3
-    : Lim_seq (fun k => exp (-1*INR k) * (RInt (fun x => (RInt (fun y => (exp x - exp y) / (x - y)) 0 (INR k))) 0 (INR k))) = putnam_1981_a3_solution.
+    : (exists r : R, Lim (fun k => exp (-1*k) * (RInt (fun x => (RInt (fun y => (exp x - exp y) / (x - y)) 0 k)) 0 k)) p_infty = r) <-> putnam_1981_a3_solution.
 Proof. Admitted.

coq/src/putnam_1982_a2.v

@@ -3,6 +3,6 @@ Open Scope R.
 Definition putnam_1982_a2_solution := True.
 Theorem putnam_1982_a2
     (B : nat -> R -> R := fun n x => sum_n (fun m => Rpower (INR m) x) n)
-    (f : nat -> R := fun n => B n (ln 2 / ln (INR n)) / (INR n) * Rpower (ln 2 / ln (INR n)) 2)
+    (f : nat -> R := fun n => B n (ln 2 / ln (INR n)) / ((INR n) * Rpower (ln 2 / ln (INR n)) 2))
     : ex_series (fun n => if (lt_dec n 2) then 0 else f n) <-> putnam_1982_a2_solution.
 Proof. Admitted.

coq/src/putnam_1982_a3.v

@@ -3,5 +3,5 @@ Open Scope R.
 Definition putnam_1982_a3_solution := PI / 2 * ln PI.
 Theorem putnam_1982_a3
     (f : R -> R := fun x => (atan (PI * x) - atan x) / x)
-    : Lim_seq (fun n => RInt f 0 (INR n)) = putnam_1982_a3_solution.
+    : Lim (fun n => RInt f 0 n) p_infty = putnam_1982_a3_solution.
 Proof. Admitted.

coq/src/putnam_1982_a5.v

@@ -2,6 +2,7 @@ Require Import Reals.
 Open Scope R.
 Theorem putnam_1982_a5 
     (a b c d: nat)
+    (hpos : Nat.lt 0 a /\ Nat.lt 0 b /\ Nat.lt 0 c /\ Nat.lt 0 d)
     (habcd : Nat.le (Nat.add a c) 1982 /\ INR a / INR b + INR c / INR d < 1)
     : 1 - INR a / INR b - INR c / INR d > 1/pow 1983 3.
 Proof. Admitted.

coq/src/putnam_1982_a6.v

@@ -3,7 +3,7 @@ Open Scope R.
 Definition putnam_1982_a6_solution := False.
 Theorem putnam_1982_a6
     (a: nat -> R) 
-    : (Series a = 1 /\ forall (i j: nat), le i j -> Rabs (a i) > Rabs (a j)) /\
-    forall (f: nat -> nat), Lim_seq (fun i => Rabs (INR (f i - i)) * Rabs (a i)) = 0 ->
-    Series (fun i => a (f i)) = 1 -> putnam_1982_a6_solution.    
+    : ((Series a = 1 /\ forall (i j: nat), le i j -> Rabs (a i) > Rabs (a j)) /\
+    forall (f: nat -> nat), Lim_seq (fun i => Rabs (INR (f i - i)) * Rabs (a i)) = 0 -> exists f', forall x, f' (f x) = x /\ f (f' x) = x -> 
+    Series (fun i => a (f i)) = 1) <-> putnam_1982_a6_solution.    
 Proof. Admitted.