Removed unnecessary lines.

coq/src/putnam_1979_a2.v

@@ -1,10 +1,3 @@
-(* Require Import Basics Reals Coquelicot.Coquelicot.
-Definition putnam_1979_a2_solution (k : R) := k >= 0. 
-Theorem putnam_1979_a2
-    : forall (k: R), (exists (f: R -> R), continuity f /\ forall x, (compose f f) x = k * pow x 9)
-    <-> putnam_1979_a2_solution k.
-Proof. Admitted. *)
-
 From mathcomp Require Import all_algebra all_ssreflect.
 From mathcomp Require Import reals topology sequences derive normedtype realfun real_interval.
 From mathcomp Require Import classical_sets.
@@ -18,8 +11,6 @@ Local Open Scope classical_set_scope.
 
 Import numFieldNormedType.Exports.
 
-About continuous.
-
 Variable R : realType.
 Definition putnam_1979_a2_solution : set R := [set x : R | x >= 0].
 Theorem putnam_1979_a2

coq/src/putnam_1979_b6.v

@@ -1,16 +1,14 @@
-Require Import Reals List Coquelicot.Coquelicot.
-Open Scope R.
-Theorem putnam_1979_b6
-    (n: nat) 
-    (l: list C)
-    (hl : length l = n)
-    (sum1 := fold_left (fun acc x => Cplus acc (Cmult x x)) l 0)
-    (sum2 := fold_left (fun acc x => Re x) l 0)
-    : sqrt (Re sum1) <= sum2.
-Proof. Admitted.
-
-
 From mathcomp Require Import all_algebra all_ssreflect.
 From mathcomp Require Import reals complex.
 
-About Rcomplex.
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+
+Variable R : realType.
+Theorem putnam_1979_b6
+    (l : seq R[i])
+    : `|Re (sqrtc (\sum_(z <- l) (z ^+ 2)))| <= \sum_(z <- l) `|Re z|.
+Proof. Admitted.