Merge pull request #189 from trishullab/jasper

Jasper

coq/src/commented_problems.v

@@ -133,3 +133,36 @@ Theorem putnam_2003_b5
     Triangle A' B' C' /\ dist A' B' = a /\ dist B' C' = b /\ dist C' A' = c /\
     F_to_R (signed_area A' B' C' D A' B' C') = (putnam_2003_b5_solution pt_to_R dist P Op).
 Proof. Admitted. *)
+
+(* Require Import Reals Rgeom ZArith 
+GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions 
+GeoCoq.Main.Annexes.midpoint_theorems
+GeoCoq.Main.Highschool.circumcenter.
+Context `{T2D:Tarski_2D} `{TE:@Tarski_euclidean Tn TnEQD}.
+Open Scope R.
+Definition putnam_1997_a1_solution := 28.
+Theorem putnam_1997_a1
+    (pt_to_R : Tpoint -> (R * R))
+    (dist : Tpoint -> Tpoint -> R := fun A B => let (a, b) := pt_to_R A in let (c, d) := pt_to_R B in dist_euc a b c d)
+    (A B C : Tpoint)
+    (Hp Op Mp Fp : Tpoint)
+    (l1 : dist Hp Op = 11)
+    (l2 : dist Op Mp = 5)
+    (s : Rectangle Hp Op Mp Fp)
+    (hHp : Bet A Fp Hp)
+    (hOp : is_circumcenter Op A B C)
+    (hMp : Midpoint B C Mp)
+    (hFp : Perp A C B Fp /\ Col A C Fp)
+    : dist B C = putnam_1997_a1_solution.
+Proof. Admitted. *)
+
+(* Require Import Nat Reals Coquelicot.Coquelicot ZArith.
+Theorem putnam_1997_b4
+    (a : nat -> nat -> Z)
+    (max_degree : nat -> nat)
+    (coeff : nat -> (nat -> R))
+    (hpoly : forall (m : nat) (x : R), sum_n (fun i => (coeff m i) * (x^i)) (max_degree m) = (1 + x + x^2)^m)
+    (ha : forall m n : nat, IZR (a m n) = coeff m n)
+    : forall k : nat, ge k 0 -> 0 <= (sum_n (fun i => (-1)^i * (IZR (a (Nat.sub k i) i))) (Z.to_nat (Coquelicot.Rcomplements.floor (2 * INR k / 3)))) <= 1.
+Proof. Admitted. *)
+

coq/src/putnam_1994_b4.v

@@ -8,8 +8,7 @@ Theorem putnam_1994_b4
     end)
     (Mmultn := fix Mmult_n {T : Ring} {n : nat} (A : matrix n n) (p : nat) :=
         match p with
-        | O => A
-        | S O => A
+        | O => mk_matrix n n (fun i j : nat => if Nat.eqb i j then one else zero)
         | S p' => @Mmult T n n n A (Mmult_n A p')
     end)
     (A := mk_matrix 2 2 (fun i j => 

coq/src/putnam_1996_a1.v

@@ -1,10 +1,8 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1996_a1_solution := (1 + sqrt 2) / 2.
-Theorem putnam_1996_a1 
-    (minA : R)
-    (packable : R -> R -> R -> R -> Prop := fun n1 n2 a1 a2 => (n1 + n2) <= Rmax a1 a2 /\ Rmax n1 n2 <= Rmin a1 a2)
-    (hminA : R -> R -> R -> R -> Prop := fun n1 n2 a1 a2 => a1 * a2 = minA /\ packable n1 n2 a1 a2)
-    (hminAlb : R -> R -> R -> R -> Prop :=  fun n1 n2 a1 a2 => forall (A: R), a1 * a2 = A /\ (packable n1 n2 a1 a2 -> minA <= A))
-    : (forall (n1 n2: R), pow n1 2 + pow n2 2 = 1 -> exists a1 a2 : R, hminA n1 n2 a1 a2 /\ hminAlb n1 n2 a1 a2) <-> minA =putnam_1996_a1_solution.
+Theorem putnam_1996_a1
+    (packable : R -> R -> R -> R -> Prop := (fun n1 n2 a1 a2 : R => (n1 + n2) <= Rmax a1 a2 /\ Rmax n1 n2 <= Rmin a1 a2))
+    (Aprop : R -> Prop := (fun A : R => forall n1 n2 : R, (n1 > 0 /\ n2 > 0 /\ pow n1 2 + pow n2 2 = 1) -> exists a1 a2 : R, a1 > 0 /\ a2 > 0 /\ a1 * a2 = A /\ packable n1 n2 a1 a2))
+    : Aprop putnam_1996_a1_solution /\ (forall A : R, Aprop A -> A >= putnam_1996_a1_solution).
 Proof. Admitted.

coq/src/putnam_1996_a3.v

@@ -1,10 +1,11 @@
 Require Import Nat Ensembles Finite_sets. From mathcomp Require Import fintype.
 Definition putnam_1996_a3_solution : Prop := False.
 Theorem putnam_1996_a3
-    (student_choices : nat -> Ensemble nat)
-    (hinrange : forall n : nat, Included _ (student_choices n) (fun i : nat => le 1 i /\ le i 6))
-    : putnam_1996_a3_solution <-> (exists S : Ensemble nat, Included _ S (fun i : nat => le 1 i /\ le i 20) /\ cardinal _ S 5 /\ 
-        (exists c1 c2 : nat, Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => le 1 i /\ le i 6) /\ 
-        (Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => (forall s : nat, In _ S s -> In _ (student_choices s) i)
-        \/ Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => forall s : nat, In _ S s -> ~ (In _ (student_choices s) i)))))).
+    (studentchoicesinrange : (nat -> Ensemble nat) -> Prop := (fun studentchoices : (nat -> Ensemble nat) => forall n : nat, Included _ (studentchoices n) (fun i : nat => le 1 i /\ le i 6)))
+    (studentchoicesprop : (nat -> Ensemble nat) -> Prop := (fun studentchoices : (nat -> Ensemble nat) =>
+        exists S : Ensemble nat, Included _ S (fun i : nat => le 1 i /\ le i 20) /\ cardinal _ S 5 /\ 
+        (exists c1 c2 : nat, (le 1 c1 /\ le c1 6) /\ (le 1 c2 /\ le c2 6) /\ c1 <> c2 /\
+        ((Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => forall s : nat, In _ S s -> In _ (studentchoices s) i))
+        \/ (Included _ (fun i : nat => i = c1 \/ i = c2) (fun i : nat => forall s : nat, In _ S s -> ~ (In _ (studentchoices s) i)))))))
+    : (forall studentchoices : (nat -> Ensemble nat), studentchoicesinrange studentchoices -> studentchoicesprop studentchoices) <-> putnam_1996_a3_solution.
 Proof. Admitted.

coq/src/putnam_1996_a4.v

@@ -2,10 +2,10 @@ Require Import Basics FinFun Reals Ensembles Finite_sets. From mathcomp Require
 Local Open Scope R_scope.
 Theorem putnam_1996_a4
     (A : finType)
-    (S : Ensemble (A * A * A))
-    (hSdistinct: forall a b c : A, In _ S (a, b, c) -> a <> b /\ b <> c /\ c <> a)
-    (hS1 : forall a b c : A, In _ S (a, b, c) -> In _ S (b, c, a))
-    (hS2 : forall a b c : A, In _ S (a, b, c) -> ~ (In _ S (c, b, a)))
-    (hS3 : forall a b c d : A, (In _ S (a, b, c)) /\ (In _ S (c, d, a)) <-> (In _ S (b, c, d) /\ In _ S (d, a, b)))
-    : exists g : A -> R, Injective g /\ (forall a b c : A, g a < g b /\ g b < g c -> In _ S (a, b, c)).
+    (SS : Ensemble (A * A * A))
+    (hSdistinct: forall a b c : A, In _ SS (a, b, c) -> a <> b /\ b <> c /\ c <> a)
+    (hS1 : forall a b c : A, In _ SS (a, b, c) <-> In _ SS (b, c, a))
+    (hS2 : forall a b c : A, In _ SS (a, b, c) <-> ~ (In _ SS (c, b, a)))
+    (hS3 : forall a b c d : A, (In _ SS (a, b, c) /\ In _ SS (c, d, a)) <-> (In _ SS (b, c, d) /\ In _ SS (d, a, b)))
+    : exists g : A -> R, Injective g /\ (forall a b c : A, g a < g b /\ g b < g c -> In _ SS (a, b, c)).
 Proof. Admitted.

coq/src/putnam_1996_a5.v

@@ -1,8 +1,8 @@
 Require Import Binomial Reals Znumtheory Coquelicot.Coquelicot. From mathcomp Require Import div.
 Open Scope R.
 Theorem putnam_1996_a5 
-    (p: nat)
+    (p : nat)
     (hp : prime (Z.of_nat p) /\ gt p 3)
-    (k := floor (2 * INR p / 3))
-    : exists (m: nat), sum_n (fun i => Binomial.C p (i+1)) (Z.to_nat k) = INR m * pow (INR p) 2.
+    (k : nat := Z.to_nat (floor (2 * INR p / 3)))
+    : exists (m : nat), sum_n_m (fun i => Binomial.C p i) 1 k = INR m * pow (INR p) 2.
 Proof. Admitted.

coq/src/putnam_1996_a6.v

@@ -1,8 +1,8 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1996_a6_solution (c: R) (f: R -> R) :=  if Rle_dec c (1/4) then exists (d: R), f = (fun _ => d) else forall (x: R), 0 <= x <= c -> continuity_pt f x /\ f 0 = f c /\ forall (x: R), x > 0 -> f x = f (pow x 2 + c) /\ (forall (x: R), x < 0 -> f x = f (-x)).
+Definition putnam_1996_a6_solution (c: R) (f: R -> R) :=  if Rle_dec c (1/4) then (exists (d: R), f = (fun _ => d)) else ((forall (x: R), 0 <= x <= c -> continuity_pt f x) /\ f 0 = f c /\ (forall (x: R), x > 0 -> f x = f (pow x 2 + c)) /\ (forall (x: R), x < 0 -> f x = f (-x))).
 Theorem putnam_1996_a6
     (c: R)
     (hc : c > 0)
-    : forall (f: R -> R), continuity f /\ forall (x: R), f x = pow x 2 + c <-> putnam_1996_a6_solution c f.
+    : forall (f: R -> R), (continuity f /\ (forall (x: R), f x = pow x 2 + c)) <-> putnam_1996_a6_solution c f.
 Proof. Admitted.

coq/src/putnam_1996_b2.v

@@ -1,10 +1,8 @@
-Require Import Reals Coquelicot.Coquelicot.
+Require Import Reals Coquelicot.Coquelicot. From mathcomp Require Import bigop.
 Open Scope R.
 Theorem putnam_1996_b2
-    (oddfact := fix odd_fact (n : nat) : R :=
-        match n with
-        | O => 1 
-        | S n' => (2 * INR n - 1) * odd_fact n'
-    end)
-    : forall (n: nat), gt n 0 -> pow ((2 * INR n - 1) / exp 1) ((2 * n - 1) / 2) < oddfact n < pow ((2 * INR n + 1) / exp 1) ((2 * n + 1) / 2).
+    (n : nat)
+    (prododd : R := INR (\prod_(1 <= i < (n + 1)) (2 * i - 1)))
+    (npos : gt n 0)
+    : Rpower ((2 * INR n - 1) / exp 1) ((2 * INR n - 1) / 2) < prododd < Rpower ((2 * INR n + 1) / exp 1) ((2 * INR n + 1) / 2).
 Proof. Admitted.

coq/src/putnam_1996_b3.v

@@ -1,11 +1,9 @@
-Require Import Nat List Reals Coquelicot.Coquelicot.
-Open Scope R.
-Definition putnam_1996_b3_solution : nat -> R := fun n => (2 * INR n ^ 3 + 3 * INR n ^ 2 - 11 * INR n + 18) / 6.
+Require Import Reals Coquelicot.Hierarchy Nat.
+Definition putnam_1996_b3_solution : nat -> R := (fun n => (2 * INR n ^ 3 + 3 * INR n ^ 2 - 11 * INR n + 18) / 6).
 Theorem putnam_1996_b3
-    (m: nat -> R)
-    (n: nat)
-    (hn : ge n 2)
-    (hmub : sum_n (fun i => INR ((nth i (seq 1 (S n)) 0%nat) * (nth ((i + 1) mod n) (seq 1 (S n)) 0%nat))) n <= m n)
-    (hm : sum_n (fun i => INR ((nth i (seq 1 (S n)) 0%nat) * (nth ((i + 1) mod n) (seq 1 (S n))) 0%nat)) n = m n)
-    : m = putnam_1996_b3_solution.
+    (n : nat)
+    (xset : (nat -> nat) -> Prop := (fun x : nat -> nat => forall y : nat, (le 1 y /\ le y n) -> exists! i, (le 0 i /\ le i (n - 1)) /\ x i = y))
+    (xsum : (nat -> nat) -> R := (fun x : nat -> nat => sum_n (fun i : nat => INR (x i) * INR (x ((i + 1) mod n))) (n - 1)))
+    (nge2 : ge n 2)
+    : (exists x : nat -> nat, xset x /\ xsum x = putnam_1996_b3_solution n) /\ (forall x : nat -> nat, xset x -> xsum x <= putnam_1996_b3_solution n).
 Proof. Admitted.

coq/src/putnam_1996_b4.v

@@ -4,15 +4,15 @@ Definition putnam_1996_b4_solution := False.
 Theorem putnam_1996_b4
     (Mmultn := fix Mmult_n {T : Ring} {n : nat} (A : matrix n n) (p : nat) :=
         match p with
-        | O => A
+        | O => mk_matrix n n (fun i j : nat => if Nat.eqb i j then one else zero)
         | S p' => @Mmult T n n n A (Mmult_n A p')
     end)
     (scale_c : R -> matrix 2 2 -> matrix 2 2 := fun c A =>  mk_matrix 2 2 (fun i j => c * coeff_mat 0 A i j))
     (sinA_mat : nat -> matrix 2 2 -> matrix 2 2 := fun n A => scale_c ((pow (-1) n) / INR (fact (2 * n + 1))) (Mmultn A (Nat.add (Nat.mul 2 n) 1)))
-    : exists (A: matrix 2 2), 
+    : (exists (A: matrix 2 2), 
     Series (fun n => coeff_mat 0 (sinA_mat n A) 0 0) = 1    /\
     Series (fun n => coeff_mat 0 (sinA_mat n A) 0 1) = 1996 /\
     Series (fun n => coeff_mat 0 (sinA_mat n A) 1 0) = 0    /\
-    Series (fun n => coeff_mat 0 (sinA_mat n A) 1 1) = 1    <->
+    Series (fun n => coeff_mat 0 (sinA_mat n A) 1 1) = 1)   <->
     putnam_1996_b4_solution.
 Proof. Admitted.

coq/src/putnam_1997_a3.v

@@ -1,6 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1997_a3_solution := sqrt (exp 1).
+Definition putnam_1997_a3_solution : R := sqrt (exp 1).
 Theorem putnam_1997_a3
     (evenfact := fix even_fact (n : nat) : R :=
         match n with
@@ -10,9 +10,9 @@ Theorem putnam_1997_a3
     (evenfactsqr := fix even_fact_sqr (n : nat) : R :=
         match n with
         | O => 1 
-        | S n' => pow (2 * INR n) 2 * evenfact n'
+        | S n' => pow (2 * INR n) 2 * even_fact_sqr n'
     end)
     (f : R -> R := fun x => Series (fun n => pow (-1) n * pow x (2 * n + 1) / evenfact n))
     (g : R -> R := fun x => Series (fun n => pow x (2 * n) / evenfactsqr n))
-    : Lim_seq (fun n => sum_n (fun m => RInt (fun x => f x * g x) 0 (INR m)) n) = putnam_1997_a3_solution.
+    : Lim_seq (fun t : nat => RInt (fun x => f x * g x) 0 (INR t)) = putnam_1997_a3_solution.
 Proof. Admitted.

coq/src/putnam_1997_a4.v

@@ -1,4 +1,4 @@
-(* Note: This formalization is only a statement finite groups (due to mathcomp), but the idea ot the problem does not rely on the cardinal of the group, so we include it*)
+(* Note: This formalization is only a statement finite groups (due to mathcomp), but the idea of the problem does not rely on the cardinal of the group, so we include it*)
 Require Import Basics. From mathcomp Require Import fingroup.
 Open Scope group_scope.
 Variable T : finGroupType.

coq/src/putnam_1997_a5.v

@@ -2,7 +2,7 @@ Require Import Nat Ensembles Finite_sets List Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1997_a5_solution := True.
 Theorem putnam_1997_a5
-    (E: Ensemble (list nat) := fun l => length l = 10%nat /\ sum_n (fun i => 1/ INR (nth i l 0%nat)) 10 = 1)
+    (E: Ensemble (list nat) := fun l => length l = 10%nat /\ (forall i : nat, lt i 10 -> gt (nth i l 0%nat) 0) /\ sum_n (fun i => 1/ INR (nth i l 0%nat)) 9 = 1)
     (m: nat)
-    : cardinal (list nat) E m /\ odd m = true <-> putnam_1997_a5_solution.
+    : cardinal (list nat) E m -> (odd m = true <-> putnam_1997_a5_solution).
 Proof. Admitted.

coq/src/putnam_1997_a6.v

@@ -1,15 +1,16 @@
 Require Import Binomial Nat Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1997_a6_solution (n k: nat) := Binomial.C (n - 1) (k - 1).
+Definition putnam_1997_a6_solution : nat -> nat -> R := (fun n k : nat => Binomial.C (n - 1) (k - 1)).
 Theorem putnam_1997_a6
-    (X := fix x (n: nat) (c: R) (k: nat) : R :=
+    (n : nat)
+    (maxc : R)
+    (X := fix x (c: R) (k: nat) : R :=
         match k with
         | O => 0 
         | S O => 1 
-        | S ((S k'') as k') => (c * x n c k' - INR (n - k) * x n c k'') / INR k'
+        | S ((S k'') as k') => (c * x c k' - INR (n - k) * x c k'') / INR k'
     end)
-    : forall (n: nat), exists (maxc: R), forall (c: R),
-    X n c (S n) = 0 /\ X n maxc (S n) = 0 -> c <= maxc ->
-    forall (k: nat), and (le 1 k) (le k n) -> 
-    X n c k = putnam_1997_a6_solution n k.
+    (npos : gt n 0)
+    (hmaxc : X maxc (add n 1) = 0 /\ (forall c : R, X c (add n 1) = 0 -> c <= maxc))
+    : forall (k: nat), (le 1 k /\ le k n) -> X maxc k = putnam_1997_a6_solution n k.
 Proof. Admitted.

coq/src/putnam_1997_b1.v

@@ -1,7 +1,7 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1997_b1_solution (n: nat) := INR n.
+Definition putnam_1997_b1_solution : nat -> R := (fun n : nat => INR n).
 Theorem putnam_1997_b1
     (rnd : R -> R := fun x => Rmin (Rabs (IZR (floor x) - x)) (Rabs (IZR (floor (x + 1)) - x)))
-    : forall (n: nat), gt n 0 -> sum_n (fun m => Rmin (rnd ((INR m + 1) / (6 * INR n))) (rnd ((INR m + 1) / (3 * INR n)))) (6 * n - 1) = putnam_1997_b1_solution n.
+    : forall (n: nat), gt n 0 -> sum_n_m (fun m => Rmin (rnd (INR m / (6 * INR n))) (rnd (INR m / (3 * INR n)))) 1 (6 * n - 1) = putnam_1997_b1_solution n.
 Proof. Admitted.

coq/src/putnam_1997_b2.v

@@ -1,7 +1,9 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1997_b2 
-    (f g: R -> R)
-    (habsbdd : R -> Prop := fun m => forall x, -m <= abs (f x) <= m)
-    : exists (M: R), forall (x: R), ex_derive_n f 2 x /\ g x >= 0 /\ f x + Derive_n f 2 x = -x * g x * Derive f x -> habsbdd M.
+    (f g : R -> R)
+    (hg : forall x : R, g x >= 0)
+    (hfdiff : forall x : R, ex_derive f x /\ ex_derive_n f 2 x)
+    (hfg : forall x : R, f x + Derive_n f 2 x = -x * g x * Derive f x)
+    : exists M : R, (forall x : R, -M <= abs (f x) <= M).
 Proof. Admitted.

coq/src/putnam_1997_b3.v

@@ -1,7 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot. From mathcomp Require Import div.
 Open Scope R.
-Definition putnam_1997_b3_solution (n: nat) := and (le 1 n) (le n 4) \/ and (le 20 n) (le n 24)  \/ and (le 100 n) (le n 104) \/ and (le 120 n) (le n 124).
+Definition putnam_1997_b3_solution : nat -> Prop := (fun n : nat => (le 1 n /\ le n 4) \/ (le 20 n /\ le n 24) \/ (le 100 n /\ le n 104) \/ (le 120 n /\ le n 124)).
 Theorem putnam_1997_b3
-    : forall (n: nat), gt n 0 -> exists (p q: nat), gt p 0 /\ gt q 0 /\ coprime p q = true /\
-    sum_n (fun m => 1 / INR (m + 1)) n = INR p / INR q -> neq (q mod 5) 0 -> putnam_1997_b3_solution n.
+    (n : nat)
+    (p q : nat)
+    (hn : gt n 0)
+    (hpq : gt p 0 /\ gt q 0 /\ coprime p q = true /\ sum_n_m (fun m => 1 / INR m) 1 n = INR p / INR q)
+    : neq (q mod 5) 0 <-> putnam_1997_b3_solution n.
 Proof. Admitted.

coq/src/putnam_1997_b5.v

@@ -1,9 +1,11 @@
 Require Import Nat.
-Theorem putnam_1997_b5 
-    (pown := fix pow_n (b n: nat) : nat :=
-      match n with
+Theorem putnam_1997_b5
+    (tetration := fix tetration' (b m: nat) : nat :=
+      match m with
       | O => 1
-      | S n' => b * pow_n b n'
+      | S m' => b ^ (tetration' b m')
     end)
-    : forall (n: nat), n >= 2 -> pown 2 n-1 mod n = pown 2 n-2.
+    (n : nat)
+    (hn : n >= 2)
+    : (tetration 2 n) mod n = (tetration 2 (n-1)) mod n.
 Proof. Admitted.

coq/src/putnam_1998_a3.v

@@ -1,6 +1,7 @@
-Require Import Reals Coquelicot.Derive.
+Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1998_a3
-    (f: R -> R)
-    : continuity (Derive_n f 3) -> exists (a: R), (Derive_n f 0) a * (Derive_n f 1) a * (Derive_n f 2) a * (Derive_n f 3) a >= 0.
+    (f : R -> R)
+    (hf : (forall x : R, ex_derive f x /\ ex_derive_n f 2 x /\ ex_derive_n f 3 x) /\ continuity (Derive_n f 3))
+    : exists (a: R), (Derive_n f 0) a * (Derive_n f 1) a * (Derive_n f 2) a * (Derive_n f 3) a >= 0.
 Proof. Admitted.

coq/src/putnam_1998_a4.v

@@ -1,13 +1,13 @@
 Require Import Nat ZArith Reals Coquelicot.Coquelicot.
 Open Scope nat_scope.
-Definition putnam_1998_a4_solution (n: nat) := exists (k: nat), n = 6 * k + 1.
+Definition putnam_1998_a4_solution : nat -> Prop := (fun n : nat => exists k : nat, n = 6 * k + 1).
 Theorem putnam_1998_a4
     (concatenate : nat -> nat -> nat := fun x y => Nat.pow 10 (Z.to_nat (floor (Rdiv (ln (INR y)) (ln 10))) + 1) * x + y)
     (a := fix A (n: nat) :=
         match n with
         | O => O
         | S O => 1
-        | S ((S n'') as n') => concatenate (A n') (A n'')
+        | S ((S n'') as n') => if eqb n'' O then 10 else (concatenate (A n') (A n''))
     end)
-    : forall (n: nat), a (n+1) mod 11 = 0 <-> putnam_1998_a4_solution n.
+    : forall (n: nat), n >= 1 -> ((a (n-1)) mod 11 = 0 <-> putnam_1998_a4_solution n).
 Proof. Admitted.

coq/src/putnam_1998_b1.v

@@ -1,10 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1998_b1_solution := 1.
+Definition putnam_1998_b1_solution : R := 6.
 Theorem putnam_1998_b1
-    (f : R -> R := fun x => ((x + 1 / x) ^ 6 - (x ^ 6 + 1 / (x ^ 6)) - 2) / (x + 1 / x) ^ 3 + (x ^ 3 + 1 / (x ^ 3)))
+    (f : R -> R := fun x => ((x + 1 / x) ^ 6 - (x ^ 6 + 1 / (x ^ 6)) - 2) / ((x + 1 / x) ^ 3 + (x ^ 3 + 1 / (x ^ 3))))
     (m : R)
-    (hm : exists (x: R), x > 0 -> f x = m) 
+    (hm : exists (x: R), x > 0 /\ f x = m) 
     (hmub : forall (x: R), x > 0 -> f x >= m) 
     : m = putnam_1998_b1_solution.
 Proof. Admitted.

coq/src/putnam_1998_b4.v

@@ -1,5 +1,6 @@
 Require Import Nat ZArith Reals Coquelicot.Coquelicot.
-Definition putnam_1998_b4_solution (m n: nat) := exists (m2 n2: nat), m mod (2 ^ m2) = 0%nat /\ m mod (2 ^ (m2 + 1)) <> 0%nat /\ n mod (2 ^ n2) = 0%nat /\ n mod (2 ^ n2 + 1) <> 0%nat.
+Definition putnam_1998_b4_solution : nat -> nat -> Prop := (fun m n : nat => forall m2 n2 : nat, (m mod (2 ^ m2) = 0%nat /\ m mod (2 ^ (m2 + 1)) <> 0%nat /\ n mod (2 ^ n2) = 0%nat /\ n mod (2 ^ n2 + 1) <> 0%nat) -> m2 <> n2).
 Theorem putnam_1998_b4
-    : forall (m n: nat), sum_n (fun i =>  Rpower (-1) (IZR (floor (INR i / INR m)) + IZR (floor (INR i / INR n)))) (m * n - 1) = 0 <-> putnam_1998_b4_solution m n.
+    (hsum : nat -> nat -> R := (fun m n : nat => sum_n (fun i =>  Rpower (-1) (IZR (floor (INR i / INR m)) + IZR (floor (INR i / INR n)))) (m * n - 1)))
+    : forall (m n: nat), (gt m 0 /\ gt n 0) -> (hsum m n = 0 <-> putnam_1998_b4_solution m n).
 Proof. Admitted.