From 8bd422dddb4e17d2306a866a5ddfe0d020773082 Mon Sep 17 00:00:00 2001
From: Jasper Lee <leejasper851@gmail.com>
Date: Wed, 17 Jul 2024 19:11:17 -0400
Subject: [PATCH] moved putnam_2003_b5 to commented_problems.v

---
 coq/src/commented_problems.v | 27 ++++++++++++++++++++++++++-
 coq/src/putnam_2003_b5.v     | 24 ------------------------
 2 files changed, 26 insertions(+), 25 deletions(-)
 delete mode 100644 coq/src/putnam_2003_b5.v

diff --git a/coq/src/commented_problems.v b/coq/src/commented_problems.v
index 291ce5fa..dae049dc 100644
--- a/coq/src/commented_problems.v
+++ b/coq/src/commented_problems.v
@@ -76,4 +76,29 @@ Theorem putnam_2010_a5:
             forall (a b: R -> R -> R),
                 cross_product a b = a. 
 Proof. Admitted.
-End putnam_2010_a5. *)
\ No newline at end of file
+End putnam_2010_a5. *)
+
+(* Require Import Reals 
+GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions
+GeoCoq.Axioms.Definitions
+GeoCoq.Main.Highschool.triangles.
+Context `{T2D:Tarski_2D} `{TE:@Tarski_euclidean Tn TnEQD}.
+Open Scope R.
+Definition putnam_2003_b5_solution (pt_to_R : Tpoint -> (R * R)) (dist : Tpoint -> Tpoint -> R) (P Op : Tpoint) := sqrt 3 * (1 - (dist P Op) ^ 2 - 1).
+Theorem putnam_2003_b5
+    (pt_to_R : Tpoint -> (R * R))
+    (F_to_R : F -> 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)
+    (Triangle : Tpoint -> Tpoint -> Tpoint -> Prop := fun x y z => ~ Col x y z) (* copied from GeoCoq.Axioms.euclidean_axioms *)
+    (A B C Op Op' P: Tpoint)
+    (fixpoint : dist Op Op' = R1)
+    (hABC : OnCircle A Op Op' /\ OnCircle B Op Op' /\ OnCircle C Op Op')
+    (hABC' : Main.Highschool.triangles.equilateral A B C)
+    (hp : InCircle P Op Op')
+    (a : R := dist P A)
+    (b : R := dist P B)
+    (c : R := dist P C)
+    : exists (A' B' C' : Tpoint) (D: Cs O E A' B' C'),
+    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. *)
diff --git a/coq/src/putnam_2003_b5.v b/coq/src/putnam_2003_b5.v
deleted file mode 100644
index 5ae16f2a..00000000
--- a/coq/src/putnam_2003_b5.v
+++ /dev/null
@@ -1,24 +0,0 @@
-Require Import Reals 
-GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions
-GeoCoq.Axioms.Definitions
-GeoCoq.Main.Highschool.triangles.
-Context `{T2D:Tarski_2D} `{TE:@Tarski_euclidean Tn TnEQD}.
-Open Scope R.
-Definition putnam_2003_b5_solution (pt_to_R : Tpoint -> (R * R)) (dist : Tpoint -> Tpoint -> R) (P Op : Tpoint) := sqrt 3 * (1 - (dist P Op) ^ 2 - 1).
-Theorem putnam_2003_b5
-    (pt_to_R : Tpoint -> (R * R))
-    (F_to_R : F -> 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)
-    (Triangle : Tpoint -> Tpoint -> Tpoint -> Prop := fun x y z => ~ Col x y z) (* copied from GeoCoq.Axioms.euclidean_axioms *)
-    (A B C Op Op' P: Tpoint)
-    (fixpoint : dist Op Op' = R1)
-    (hABC : OnCircle A Op Op' /\ OnCircle B Op Op' /\ OnCircle C Op Op')
-    (hABC' : Main.Highschool.triangles.equilateral A B C)
-    (hp : InCircle P Op Op')
-    (a : R := dist P A)
-    (b : R := dist P B)
-    (c : R := dist P C)
-    : exists (A' B' C' : Tpoint) (D: Cs O E A' B' C'),
-    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.
\ No newline at end of file