Isabelle & Coq verifications: 2004-2005 & 1991-1995

coq/src/putnam_1991_a2.v

@@ -4,9 +4,8 @@ Definition putnam_1991_a2_solution := False.
 Theorem putnam_1991_a2
     (R : comUnitRingType) 
     (n : nat) 
-    (A B : 'M[R]_n) 
-    (hAB : A <> B)
-    : mulmx (mulmx A A) A = mulmx (mulmx B B) B /\
-    mulmx (mulmx A A) B = mulmx (mulmx B B) A ->
-    (mulmx A A + mulmx B B) \in unitmx <-> putnam_1991_a2_solution.
+    (npos : n >= 1)
+    : (exists A B : 'M[R]_n, A <> B /\ mulmx (mulmx A A) A = mulmx (mulmx B B) B /\
+    mulmx (mulmx A A) B = mulmx (mulmx B B) A /\
+    (mulmx A A + mulmx B B) \in unitmx) <-> putnam_1991_a2_solution.
 Proof. Admitted.

coq/src/putnam_1991_a3.v

@@ -1,11 +1,14 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1991_a3_solution (coeff: nat -> R) (n: nat) : Prop := exists (A r1 r2: R), coeff = (fun x => match x with | O => A * r1 * r2 | S O => -A * (r1 + r2) | S (S O) => A | _ => 0 end) /\ n = 2%nat.
+Definition poly (coeff : nat -> R) (deg : nat) : R -> R := fun x : R => sum_n (fun i => coeff i * x ^ i) deg.
+Definition putnam_1991_a3_solution (coeff: nat -> R) : Prop := (forall n : nat, gt n 2 -> coeff n = 0) /\ exists (r1 r2 : R), r1 <> r2 /\ poly coeff 2 r1 = 0 /\ poly coeff 2 r2 = 0.
 Theorem putnam_1991_a3
-    (p: (nat -> R) -> nat -> (R -> R) := fun coeff n => (fun x => sum_n (fun i => coeff i * x ^ i) (n + 1)))
-    : forall (coeff: nat -> R) (n: nat), ge n 2 ->
-    (exists (r: nat -> R), 
-    (forall (i j: nat), lt i j -> r i < r j) /\
-    forall (i: nat), lt i n -> p coeff n (r i) = 0 /\ lt i (n - 1) -> (Derive (p coeff n)) ((r i + r (S i)) / 2) = 0) <->
-    putnam_1991_a3_solution coeff n.
+    (coeff : nat -> R)
+    (n : nat)
+    (hn : coeff n <> 0 /\ forall m : nat, gt m n -> coeff m = 0)
+    (hge : ge n 2)
+    : (exists (r: nat -> R), (forall i : nat, lt i (n - 1) -> r i < r (S i)) /\
+    (forall i : nat, lt i n -> poly coeff n (r i) = 0) /\ 
+    (forall i : nat, lt i (n - 1) -> (Derive (poly coeff n)) ((r i + r (S i)) / 2) = 0)) <->
+    putnam_1991_a3_solution coeff.
 Proof. Admitted.

coq/src/putnam_1991_a5.v

@@ -2,8 +2,6 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1991_a5_solution := 1/3.
 Theorem putnam_1991_a5
-    (m: R)
-    (hm : exists (y: R), 0 <= y <= 1 -> m >= RInt (fun x => sqrt (pow x 4 + pow (y - pow y 2) 2)) 0 y)
-    (hmub : forall (y: R), 0 <= y <= 1 -> m >= RInt (fun x => sqrt (pow x 4 + pow (y - pow y 2) 2)) 0 y)
-    : m = putnam_1991_a5_solution.
+    (f : R -> R := fun y : R => RInt (fun x => sqrt (pow x 4 + pow (y - pow y 2) 2)) 0 y)
+    : (exists (y : R), 0 <= y <= 1 /\ putnam_1991_a5_solution = f y) /\ (forall (y : R), 0 <= y <= 1 -> putnam_1991_a5_solution >= f y).
 Proof. Admitted.

coq/src/putnam_1991_b1.v

@@ -1,4 +1,4 @@
-Require Import Nat Coquelicot.Coquelicot.
+Require Import Nat.
 Open Scope nat_scope.
 Definition putnam_1991_b1_solution (A: nat) := exists (m: nat), A = pow m 2.
 Theorem putnam_1991_b1
@@ -8,5 +8,7 @@ Theorem putnam_1991_b1
         | O => A
         | S k' => a A k' + eS (a A k')
     end)
-    : forall (A: nat), A > 0 -> Lim_seq (fun k => Raxioms.INR (a_seq A k)) = Rdefinitions.R0 <-> putnam_1991_b1_solution A.
+    (A : nat)
+    (hA : gt A 0)
+    : (exists K c : nat, forall k : nat, k >= K -> a_seq A k = c) <-> putnam_1991_b1_solution A.
 Proof. Admitted.

coq/src/putnam_1991_b2.v

@@ -1,8 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1991_b2
-    (f g: R -> R)
-    (hfg : ~ exists (c: R), f = (fun _ => c) \/ g = (fun _ => c) /\ forall x, ex_derive_n f 1 x /\ forall x, ex_derive_n g 1 x)
-    : forall (x y: R), f (x + y) = f x * f y - g x * g y /\ g (x + y) = f x * g y - g x * f y ->
-    Derive f 0 = 0 -> forall (x: R), pow (f x) 2 + pow (g x) 2 = 1.
+    (f g : R -> R)
+    (fgnconst : ~ exists (c : R), f = (fun _ => c) \/ g = (fun _ => c))
+    (fgdiff : forall x : R, ex_derive f x /\ ex_derive g x)
+    (fadd : forall x y : R, f (x + y) = f x * f y - g x * g y)
+    (gadd : forall x y : R, g (x + y) = f x * g y + g x * f y)
+    : Derive f 0 = 0 -> forall x : R, pow (f x) 2 + pow (g x) 2 = 1.
 Proof. Admitted.

coq/src/putnam_1991_b5.v

@@ -4,8 +4,8 @@ Definition putnam_1991_b5_solution (p: nat) : nat := p / 4 + 1.
 Theorem putnam_1991_b5 
     (p: nat)
     (hp : odd p = true /\ prime (Z.of_nat p))
-    (A: Ensemble Z := fun z => exists (m: 'I_p), z = Z.of_nat (pow (nat_of_ord m) 2))
-    (B: Ensemble Z := fun z => exists (m: 'I_p), z = Z.of_nat (pow (nat_of_ord m) 2 + 1))
+    (A: Ensemble Z := fun z => exists (m: 'I_p), z = Z.of_nat (pow (nat_of_ord m) 2) mod (Z.of_nat p))
+    (B: Ensemble Z := fun z => exists (m: 'I_p), z = Z.of_nat (pow (nat_of_ord m) 2 + 1) mod (Z.of_nat p))
     (C : Ensemble Z := Intersection Z A B)
     : cardinal Z C (putnam_1991_b5_solution p).
 Proof. Admitted.

coq/src/putnam_1991_b6.v

@@ -1,10 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1991_b6_solution (a b : R) := IZR (floor (ln (a / b))). 
+Definition putnam_1991_b6_solution (a b : R) := Rabs (ln (a / b)). 
 Theorem putnam_1991_b6 
     (a b: R)
     (hab : a > 0 /\ b > 0)
-    (ineq_holds : R -> Prop := fun c => forall (u x: R), 0 < Rabs u <= c /\ 0 < x < 1 -> Rpower a x * Rpower b (1 - x) <= a * sinh (u * x) / sinh u + b * sinh (1 - x) / sinh u)
+    (ineq_holds : R -> Prop := fun c => forall (u x: R), 0 < Rabs u <= c /\ 0 < x < 1 -> Rpower a x * Rpower b (1 - x) <= a * sinh (u * x) / sinh u + b * sinh (u * (1 - x)) / sinh u)
     (c: R)
     (hc : ineq_holds c)
     (hcub : forall (x: R), ineq_holds x -> x <= c)

coq/src/putnam_1992_a1.v

@@ -1,6 +1,6 @@
-Require Import Basics.
+Require Import Basics ZArith.
+Open Scope Z_scope.
 Theorem putnam_1992_a1 
-    (f : nat -> nat) 
-    (hf : forall (n: nat), f (f n) = n /\ f (f (n + 2)) + 2 = n /\ f 0 = 1)
-    : f = (fun n => 1 - n).
+    (f : Z -> Z) 
+    : f = (fun n => 1 - n) <-> ((forall n : Z, f (f n) = n) /\ (forall n : Z, f (f (n + 2) + 2) = n) /\ f 0 = 1).
 Proof. Admitted.

coq/src/putnam_1992_a2.v

@@ -3,5 +3,5 @@ Open Scope R.
 Definition putnam_1992_a2_solution := 1992.
 Theorem putnam_1992_a2
     (C : R -> R := fun a => (Derive_n (fun x => Rpower (1 + x) a) 1992) 0 / INR (fact 1992))
-    : RInt (fun y => C( - y - 1 ) * (sum_n (fun k => 1 / (y + INR k)) 1992)) 0 1 = putnam_1992_a2_solution.
+    : RInt (fun y => C (-y - 1) * sum_n_m (fun k => 1 / (y + INR k)) 1 1992) 0 1 = putnam_1992_a2_solution.
 Proof. Admitted.

coq/src/putnam_1992_a3.v

@@ -1,8 +1,8 @@
 Require Import Nat. From mathcomp Require Import div fintype perm ssrbool.
-Definition putnam_1992_a3_solution (x y n m: nat) := exists r, x = 2 ^ r /\ y = 2 ^ r /\ n = 2 * r /\ m = 2 * r + 1.
+Definition putnam_1992_a3_solution (x y n m: nat) := exists r, x = 2 ^ r /\ y = 2 ^ r /\ n = 2 * r + 1 /\ m = 2 * r.
 Theorem putnam_1992_a3
     (m : nat)
     (hm : m > 0)
-    (hnxy : nat -> nat -> nat -> Prop := fun n x y => n > 0 /\ x > 0 /\ y > 0 /\ coprime n m /\ pow (pow x 2 + pow y 2) m = pow (x * y) m)
-    : forall n x y, putnam_1992_a3_solution x y n m.
+    (hnxy : nat -> nat -> nat -> Prop := fun n x y => n > 0 /\ x > 0 /\ y > 0 /\ coprime n m /\ pow (pow x 2 + pow y 2) m = pow (x * y) n)
+    : forall n x y, putnam_1992_a3_solution x y n m <-> hnxy n x y.
 Proof. Admitted.

coq/src/putnam_1992_a4.v

@@ -1,8 +1,9 @@
 Require Import Nat Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1992_a4_solution (k: nat) := if odd k then 0 else pow (-1) (k/2).
+Definition putnam_1992_a4_solution (k : nat) := if odd k then 0 else pow (-1) (k/2) * INR (fact k).
 Theorem putnam_1992_a4
-    (f : R -> R := fun n => (pow (1 / n) 2) / ((pow (1 / n) 2) + 1))
-    (df_0 : nat -> R := fun k => (Derive_n f k) 0)
-    : forall (k: nat), gt k 0 -> df_0 k = putnam_1992_a4_solution k.
+    (f : R -> R)
+    (hfdiff : forall k : nat, continuity (Derive_n f k) /\ forall x : R, ex_derive (Derive_n f k) x)
+    (hf : forall n : nat, gt n 0 -> f (1 / INR n) = (INR n)^2 / ((INR n)^2 + 1))
+    : forall (k : nat), gt k 0 -> (Derive_n f k) 0 = putnam_1992_a4_solution k.
 Proof. Admitted.

coq/src/putnam_1992_a5.v

@@ -1,5 +1,4 @@
 Require Import BinPos Nat ZArith.
-Definition putnam_1992_a5_solution := 1.
 Theorem putnam_1992_a5
     (k := fix count_ones (n : positive) : nat :=
         match n with
@@ -8,5 +7,5 @@ Theorem putnam_1992_a5
         | xI n' => 1 + count_ones n'
     end)
     (a : positive -> nat := fun n => (k n) mod 2)
-    : ~ exists (k m: nat), forall (j: nat), 0 <= j <= m - 1 -> a (Pos.of_nat (k + j)) = a (Pos.of_nat (k + m + j)) /\ a (Pos.of_nat (k + m + j)) = a (Pos.of_nat (k + 2 * m + j)).
+    : ~ exists (k m: nat), gt k 0 /\ gt m 0 /\ forall (j: nat), j <= m - 1 -> a (Pos.of_nat (k + j)) = a (Pos.of_nat (k + m + j)) /\ a (Pos.of_nat (k + m + j)) = a (Pos.of_nat (k + 2 * m + j)).
 Proof. Admitted.

coq/src/putnam_1992_b1.v

@@ -2,10 +2,11 @@ Require Import Nat Ensembles Finite_sets Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1992_b1_solution (n: nat) := sub (mul 2 n) 3.
 Theorem putnam_1992_b1
-    (n : nat) 
-    (E : Ensemble R)
-    (AE_criterion : Ensemble R -> Ensemble R -> Prop := fun E AE => cardinal R E n /\ forall (m: R), AE m <-> exists (p q: R), E p /\ E q /\ m = (p + q) / 2)
-    : gt n 2 -> exists (minAE: nat), 
-    (forall (AE: Ensemble R) (szAE: nat), cardinal R AE szAE /\ cardinal R AE minAE -> ge szAE minAE) <->
-    minAE = putnam_1992_b1_solution n.
+    (n : nat)
+    (nge2 : ge n 2)
+    (A : Ensemble R -> Ensemble R := fun E : Ensemble R => fun x : R => exists a b : R, E a /\ E b /\ a <> b /\ (a + b) / 2 = x)
+    (min : nat)
+    (hmineq : exists E : Ensemble R, cardinal R E n /\ cardinal R (A E) min)
+    (hminlb : forall E : Ensemble R, cardinal R E n -> exists m : nat, le m min /\ cardinal R (A E) m)
+    : min = putnam_1992_b1_solution n.
 Proof. Admitted.

coq/src/putnam_1992_b4.v

@@ -2,11 +2,17 @@ From mathcomp Require Import ssrnat ssrnum ssralg poly polydiv seq.
 Open Scope ring_scope.
 Definition putnam_1992_b4_solution := 3984%nat.
 Theorem putnam_1992_b4
-    (R : numDomainType) 
-    (p : {poly R})
-    (cond : {poly R} -> {poly R} -> Prop := fun f g => derivn 1992 (p %/ ('X^3 - 'X)) = f %/ g)
-    : gt (size p) 1992 /\ exists c: R, gcdp_rec p ('X^3 - 'X) = polyC c ->
-    exists mindeg, ((forall (f g: {poly R}), cond f g /\ ge (size f) mindeg) /\ 
-    (exists (f g: {poly R}), cond f g /\ size f = mindeg)) <->
-    mindeg = putnam_1992_b4_solution.
+    (R : numDomainType)
+    (itercomp := fix iter (f : {poly R} * {poly R} -> {poly R} * {poly R}) (n : nat) (p : {poly R} * {poly R}) : {poly R} * {poly R} :=
+        match n with
+        | O => p
+        | S n' => f (iter f n' p)
+    end)
+    (qr : {poly R} * {poly R} -> {poly R} * {poly R} := fun duple => (deriv (fst duple) * snd duple - deriv (snd duple) * fst duple, snd duple * snd duple))
+    (valid : {poly R} -> Prop := fun p => p <> 0 /\ lt (size p) 1992 /\ exists c : R, gcdp_rec p ('X^3 - 'X) = polyC c)
+    (twople : {poly R} -> {poly R} -> Prop := fun p f => exists g : {poly R}, g * fst (itercomp qr 1992%nat (p, 'X^3 - 'X)) = f * snd (itercomp qr 1992%nat (p, 'X^3 - 'X)))
+    (min : nat)
+    (hmineq : exists p f : {poly R}, (valid p /\ twople p f) /\ size f = min)
+    (hminlb : forall p f : {poly R}, (valid p /\ twople p f) -> ge (size f) min)
+    : min = putnam_1992_b4_solution.
 Proof. Admitted.

coq/src/putnam_1993_a2.v

@@ -2,8 +2,7 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1993_a2 
     (x : nat -> R)
-    (n : nat)
-    (hn : gt n 0)
-    : pow (x n) 2 - x (pred n) * x (S n) = 1 ->
-    exists (a: R), ge n 1 -> x (S n) = a * x n - x (pred n).
+    (xnonzero : forall n : nat, x n <> 0)
+    (hx : forall n : nat, ge n 1 -> pow (x n) 2 - x (pred n) * x (S n) = 1)
+    : exists a : R, forall n : nat, ge n 1 -> x (S n) = a * x n - x (pred n).
 Proof. Admitted.

coq/src/putnam_1993_a4.v

@@ -1,16 +1,13 @@
 Require Import List Bool Reals Peano_dec Coquelicot.Coquelicot.
 Open Scope nat_scope.
+Fixpoint s_sum (a : nat -> nat) (k : nat) (s : nat -> bool) : nat := 
+    match k with
+    | O => a 0
+    | S k' => (if s k then a k else 0) + s_sum a k' s
+    end.
 Theorem putnam_1993_a4 
-    (x y: list nat)
-    (hx : length x = 19)
-    (hy : length y = 93)
-    (hx2 : forall n : nat, In n x -> 1 < n <= 93)
-    (hy2 : forall n  : nat, In n y -> 1 < n <= 19)
-    : exists (presentx presenty : nat -> bool), 
-    sum_n (fun n => 
-        if ((existsb (fun i => if eq_nat_dec n i then true else false) x) && presentx n) 
-        then (INR n) else R0) 94 = 
-    sum_n (fun n => 
-        if ((existsb (fun i => if eq_nat_dec n i then true else false) y) && presenty n) 
-        then (INR n) else R0) 20. 
+    (x y : nat -> nat)
+    (hx : forall i : nat, i < 19 -> 1 <= x i <= 93)
+    (hy : forall j : nat, j < 93 -> 1 <= y j <= 19)
+    : exists (is js : nat -> bool), (exists i : nat, i < 19 /\ is i = true) /\ s_sum x 18 is = s_sum y 92 js.
 Proof. Admitted.

coq/src/putnam_1993_b1.v

@@ -2,7 +2,6 @@ Require Import Reals.
 Open Scope R.
 Definition putnam_1993_b1_solution : nat := 3987.
 Theorem putnam_1993_b1
-    (cond : nat -> Prop := fun n => forall (m: nat), and (lt 0 m) (lt m 1993) -> exists (k: nat), INR m / 1993 < INR k / INR n < INR (m + 1) / 1994)
-    : exists (mn : nat), cond mn /\ forall (n: nat), cond n -> ge n mn <->
-    mn = putnam_1993_b1_solution.
+    (cond : nat -> Prop := fun n => gt n 0 /\ forall (m: nat), and (lt 0 m) (lt m 1993) -> exists (k: nat), INR m / 1993 < INR k / INR n < INR (m + 1) / 1994)
+    : cond putnam_1993_b1_solution /\ forall (n: nat), cond n -> ge n putnam_1993_b1_solution.
 Proof. Admitted.

coq/src/putnam_1993_b4.v

@@ -1,12 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1993_b4 
-    (K: (R * R) -> R) 
-    (f g: R -> R)
-    (hK : forall (xy : R * R), let (x, y) := xy in 0 <= x <= 1 /\ 0 <= y <= 1 /\ K xy > 0 /\ continuous K xy)
-    (hfg : forall (x: R), 0 <= x <= 1 /\ f x > 0 /\ g x > 0 /\ continuity f /\ continuity g ->
-        forall (x: R), 0 <= x <= 1 -> 
-        (RInt (fun y => f y * K (x, y)) 0 1) = g x /\
-        RInt (fun y => g y * K (x, y)) 0 1 = f x)
-    : forall (x: R), 0 <= x <= 1 -> f x = g x.
+    (K : (R * R) -> R) 
+    (f g : R -> R)
+    (hK : forall x y : R, 0 <= x <= 1 /\ 0 <= y <= 1 -> K (x, y) > 0 /\ continuous K (x, y))
+    (hfg : forall x : R, 0 <= x <= 1 -> f x > 0 /\ g x > 0 /\ continuous f x /\ continuous g x /\
+        RInt (fun y => f y * K (x, y)) 0 1 = g x /\ RInt (fun y => g y * K (x, y)) 0 1 = f x)
+    : forall x : R, 0 <= x <= 1 -> f x = g x.
 Proof. Admitted.

coq/src/putnam_1994_a1.v

@@ -1,6 +1,7 @@
 Require Import Nat Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1994_a1
-    : exists (a: nat -> R), forall (n: nat), gt n 0 -> 0 < a n <= a (mul 2 n) + a (add (mul 2 n) 1) ->
-    ~ ex_lim_seq (fun n => sum_n (fun m => a m) n).
+    (a : nat -> R)
+    (ha : forall n : nat, gt n 0 -> 0 < a n <= a (mul 2 n) + a (add (mul 2 n) 1))
+    : ~ ex_finite_lim_seq (fun n => sum_n (fun m => a m) n).
 Proof. Admitted.

coq/src/putnam_1994_b1.v

@@ -2,7 +2,7 @@ Require Import Ensembles Finite_sets ZArith.
 Open Scope Z.
 Definition putnam_1994_b1_solution (n: Z) := 315 <= n <= 325 \/ 332 <= n <= 350.
 Theorem putnam_1994_b1
-    : forall (n: Z), exists (E: Ensemble Z), cardinal Z E 15 -> 
-    forall (m: Z), E m -> Z.abs (m * m - n) <= 250 ->
-    putnam_1994_b1_solution n.
+    (n : Z)
+    (nwithin : Prop := cardinal nat (fun m => Z.abs (n - (Z.of_nat m) ^ 2) <= 250) 15)
+    : (n > 0 /\ nwithin) <-> putnam_1994_b1_solution n.
 Proof. Admitted.

coq/src/putnam_1994_b2.v

@@ -1,9 +1,7 @@
-Require Import List Reals Coquelicot.Coquelicot.
+Require Import Ensembles Reals Finite_sets Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1994_b2_solution (c: R) := c < 243 / 8.
 Theorem putnam_1994_b2
-    (f : R -> R -> R := fun c x => pow x 4 + 9 * pow x 3 + c * pow x 2 + 9 * x + 4)
-    (g : R -> R -> R -> R := fun m x b  => m * x + b)
-    (hintersect : R -> Prop := fun c => exists(m b: R), exists (l: list R), eq (length l) 4%nat /\ NoDup l /\ forall (r: R), In r l -> f c r = g m b r)
+    (hintersect : R -> Prop := fun c => exists(m b: R), cardinal R (fun x => m * x + b = pow x 4 + 9 * pow x 3 + c * pow x 2 + 9 * x + 4) 4)
     : forall (c: R), hintersect c <-> putnam_1994_b2_solution c.
 Proof. Admitted.

coq/src/putnam_1994_b3.v

@@ -1,7 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1994_b3_solution (k: R) := k <= 1.
+Definition putnam_1994_b3_solution (k: R) := k < 1.
 Theorem putnam_1994_b3
-    : forall (k: R) (f: R -> R) (x: R), f x > 0 /\ ex_derive f x /\ (Derive f) x > f x ->
-    exists (N: R), x > N -> f x > exp (k * x) <-> putnam_1994_b3_solution k.
+    : forall k : R, (forall f : R -> R, (forall x : R, f x > 0 /\ ex_derive f x /\ (Derive f) x > f x) -> exists N : R, forall x : R, x > N -> f x > exp (k * x)) <-> putnam_1994_b3_solution k.
 Proof. Admitted.

coq/src/putnam_1994_b4.v

@@ -1,6 +1,5 @@
 Require Import Nat List Reals Coquelicot.Coquelicot. 
 Import ListNotations.
-Open Scope R.
 Theorem putnam_1994_b4 
     (gcdn := fix gcd_n (args : list nat) : nat :=
         match args with
@@ -10,6 +9,7 @@ Theorem putnam_1994_b4
     (Mmultn := fix Mmult_n {T : Ring} {n : nat} (A : matrix n n) (p : nat) :=
         match p with
         | O => A
+        | S O => A
         | S p' => @Mmult T n n n A (Mmult_n A p')
     end)
     (A := mk_matrix 2 2 (fun i j => 
@@ -29,5 +29,5 @@ Theorem putnam_1994_b4
                               Z.to_nat (floor (coeff_mat 0 (dn_mat n) 0 1)); 
                               Z.to_nat (floor (coeff_mat 0 (dn_mat n) 1 0)); 
                               Z.to_nat (floor (coeff_mat 0 (dn_mat n) 1 1))])
-    : ~ ex_lim_seq (fun n => INR (dn n)).
+    : forall k : nat, exists N : nat, forall n : nat, ge n N -> ge (dn n) k.
 Proof. Admitted.

coq/src/putnam_1994_b5.v

@@ -1,11 +1,11 @@
 Require Import Basics ZArith Zpower Reals Coquelicot.Coquelicot.
+Open Scope Z_scope.
 Theorem putnam_1994_b5
     (composen := fix compose_n {A: Type} (f : A -> A) (n : nat) :=
         match n with
         | O => fun x => x
         | S n' => compose f (compose_n f n')
     end)
-    (fa : R -> R -> R := fun a x => IZR (floor (a * x)))
-    : forall (n: Z), Z.gt n 0 ->
-    exists (a: R), forall (k: Z), and (Z.ge 1 k) (Z.ge k n) -> (composen (fa a) (Z.to_nat k)) (IZR (Z.pow n 2)) = IZR (Z.pow n 2 - k) /\ IZR (Z.pow n 2 - k) = fa (Rpower a (IZR k)) (IZR (Z.pow n 2)).
+    (fa : R -> Z -> Z := fun a x => floor (a * IZR x))
+    : forall (n: Z), n > 0 -> exists (a: R), forall (k: Z), 1 <= k <= n -> (composen (fa a) (Z.to_nat k)) n^2 = n^2 - k /\ n^2 - k = fa (Rpower a (IZR k)) n^2.
 Proof. Admitted.

coq/src/putnam_1994_b6.v

@@ -1,6 +1,7 @@
-Require Import Nat.
+Require Import ZArith.
+Open Scope Z_scope.
 Theorem putnam_1994_b6
-    (n : nat -> nat := fun a => 101 * a -  100 * pow 2 a)
-    : forall a b c d : nat, 0 <= a <= 99 /\ 0 <= b <= 99 /\  0 <= c <= 99 /\  0 <= d <= 99 /\ n a + n b mod 10100 = n c + n d ->
-    (a,b) = (c,d).
+    (n : Z -> Z := fun a => 101 * a - 100 * 2^a)
+    : forall a b c d : Z, 0 <= a <= 99 /\ 0 <= b <= 99 /\ 0 <= c <= 99 /\ 0 <= d <= 99 /\ 
+    (n a + n b) mod 10100 = (n c + n d) mod 10100 -> (a = c /\ b = d) \/ (a = d /\ b = c).
 Proof. Admitted.

coq/src/putnam_1995_a1.v

@@ -1,11 +1,11 @@
 Require Import Reals Ensembles Coquelicot.Coquelicot.
 Theorem putnam_1995_a1
-    (S T U : Ensemble R)
-    (hS : forall a : R, forall b : R, In _ S a /\ In _ S b -> In _ S (a * b))
-    (hsub : Included _ T S /\ Included _ U S)
-    (hunion : Same_set _ (Union _ T U) S)
+    (E T U : Ensemble R)
+    (hE : forall a : R, forall b : R, In _ E a /\ In _ E b -> In _ E (a * b))
+    (hsub : Included _ T E /\ Included _ U E)
+    (hunion : Same_set _ (Union _ T U) E)
     (hdisj : Disjoint _ T U)
     (hT3 : forall a b c : R, In _ T a /\ In _ T b /\ In _ T c -> In _ T (a * b * c))
-    (hS3 : forall a b c : R, In _ S a /\ In _ S b /\ In _ S c -> In _ S (a * b * c))
+    (hU3 : forall a b c : R, In _ U a /\ In _ U b /\ In _ U c -> In _ U (a * b * c))
     : (forall a b : R, In _ T a /\ In _ T b -> In _ T (a * b)) \/ (forall a b : R, In _ U a /\ In _ U b -> In _ U (a * b)).
 Proof. Admitted.

coq/src/putnam_1995_a2.v

@@ -2,5 +2,5 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1995_a2_solution : R -> R -> Prop := fun (a b: R) => a = b.
 Theorem putnam_1995_a2
-    : forall (a b: R), a > 0 /\ b > 0 /\ ex_finite_lim_seq (fun n => RInt (fun x => sqrt (sqrt (x + a) - sqrt x) - sqrt (sqrt x - (x - b))) b (INR n)) <-> putnam_1995_a2_solution a b.
+    : forall (a b: R), a > 0 /\ b > 0 -> ((exists limit : R, filterlim (fun n : R => RInt (fun x => sqrt (sqrt (x + a) - sqrt x) - sqrt (sqrt x - (x - b))) b n) (Rbar_locally p_infty) (locally limit)) <-> putnam_1995_a2_solution a b).
 Proof. Admitted.