From fa29e4237e581e4d3e4fa1c799dc5275a8678171 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Wed, 29 May 2024 09:43:45 -0500
Subject: [PATCH 1/9] add docker

---
 .dockerignore |  5 +++++
 Dockerfile    | 40 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+)
 create mode 100644 .dockerignore
 create mode 100644 Dockerfile

diff --git a/.dockerignore b/.dockerignore
new file mode 100644
index 0000000..09a8c39
--- /dev/null
+++ b/.dockerignore
@@ -0,0 +1,5 @@
+.vscode
+tmp
+.lake
+python/__pycache__
+*/.DS_Store
\ No newline at end of file
diff --git a/Dockerfile b/Dockerfile
new file mode 100644
index 0000000..888ad45
--- /dev/null
+++ b/Dockerfile
@@ -0,0 +1,40 @@
+FROM ubuntu:latest
+
+WORKDIR /LeanEuclid
+COPY . .
+
+# Install dependencies.
+RUN apt-get update && apt-get install -y curl git python3 python3-pip
+
+# Install elan.
+ENV ELAN_HOME="/.elan"
+ENV PATH="${ELAN_HOME}/bin:${PATH}"
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
+
+# Build and Install CVC5.
+RUN git clone https://github.com/cvc5/cvc5
+WORKDIR cvc5
+RUN ./configure.sh --auto-download
+WORKDIR build
+RUN make -j$(nproc)
+RUN sudo make install
+WORKDIR /LeanEuclid
+
+# Build and Install Z3.
+RUN git clone https://github.com/Z3Prover/z3
+WORKDIR z3
+RUN python3 scripts/mk_make.py
+WORKDIR build
+RUN make -j$(nproc)
+RUN sudo make install
+WORKDIR /LeanEuclid
+
+# Install smt-portfolio.
+RUN pip3 install --upgrade pip
+RUN pip3 install smt-portfolio
+
+# Build the Lean project.
+RUN lake script run check
+RUN lake exe cache get
+RUN lake build SystemE Book UniGeo E3
+RUN lake -R -Kenv=dev build SystemE:docs

From b9651b9464bd98d280ea48d8b8179de097ae523d Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Wed, 29 May 2024 09:44:53 -0500
Subject: [PATCH 2/9] add cmake to docker

---
 Dockerfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Dockerfile b/Dockerfile
index 888ad45..0672f8d 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -4,7 +4,7 @@ WORKDIR /LeanEuclid
 COPY . .
 
 # Install dependencies.
-RUN apt-get update && apt-get install -y curl git python3 python3-pip
+RUN apt-get update && apt-get install -y curl git cmake python3 python3-pip
 
 # Install elan.
 ENV ELAN_HOME="/.elan"

From bfa656e2dc2d452db70d9260f6a445524c47eecf Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Wed, 29 May 2024 09:47:17 -0500
Subject: [PATCH 3/9] add venv to docker

---
 Dockerfile | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index 0672f8d..db06e3b 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -4,12 +4,7 @@ WORKDIR /LeanEuclid
 COPY . .
 
 # Install dependencies.
-RUN apt-get update && apt-get install -y curl git cmake python3 python3-pip
-
-# Install elan.
-ENV ELAN_HOME="/.elan"
-ENV PATH="${ELAN_HOME}/bin:${PATH}"
-RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
+RUN apt-get update && apt-get install -y curl git cmake python3-venv python3-pip
 
 # Build and Install CVC5.
 RUN git clone https://github.com/cvc5/cvc5
@@ -33,6 +28,11 @@ WORKDIR /LeanEuclid
 RUN pip3 install --upgrade pip
 RUN pip3 install smt-portfolio
 
+# Install elan.
+ENV ELAN_HOME="/.elan"
+ENV PATH="${ELAN_HOME}/bin:${PATH}"
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
+
 # Build the Lean project.
 RUN lake script run check
 RUN lake exe cache get

From a26dfd7f17d4e402fb58146b7361ba2cf38e6a9f Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Wed, 29 May 2024 09:53:14 -0500
Subject: [PATCH 4/9] add m4 to docker

---
 Dockerfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Dockerfile b/Dockerfile
index db06e3b..961bbfe 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -4,7 +4,7 @@ WORKDIR /LeanEuclid
 COPY . .
 
 # Install dependencies.
-RUN apt-get update && apt-get install -y curl git cmake python3-venv python3-pip
+RUN apt-get update && apt-get install -y curl git cmake m4 python3-venv python3-pip
 
 # Build and Install CVC5.
 RUN git clone https://github.com/cvc5/cvc5

From 18e6fae714ae7710fc3cbb31ae01f82a0b219990 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Wed, 29 May 2024 09:55:48 -0500
Subject: [PATCH 5/9] use fewer threads

---
 Dockerfile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index 961bbfe..82ba42a 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -11,7 +11,7 @@ RUN git clone https://github.com/cvc5/cvc5
 WORKDIR cvc5
 RUN ./configure.sh --auto-download
 WORKDIR build
-RUN make -j$(nproc)
+RUN make -j8
 RUN sudo make install
 WORKDIR /LeanEuclid
 
@@ -20,7 +20,7 @@ RUN git clone https://github.com/Z3Prover/z3
 WORKDIR z3
 RUN python3 scripts/mk_make.py
 WORKDIR build
-RUN make -j$(nproc)
+RUN make -j8
 RUN sudo make install
 WORKDIR /LeanEuclid
 

From b2b8daf7f261080497a07c060974c020615178ba Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Wed, 29 May 2024 09:56:32 -0500
Subject: [PATCH 6/9] remove sudo

---
 Dockerfile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index 82ba42a..b8885d9 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -12,7 +12,7 @@ WORKDIR cvc5
 RUN ./configure.sh --auto-download
 WORKDIR build
 RUN make -j8
-RUN sudo make install
+RUN make install
 WORKDIR /LeanEuclid
 
 # Build and Install Z3.
@@ -21,7 +21,7 @@ WORKDIR z3
 RUN python3 scripts/mk_make.py
 WORKDIR build
 RUN make -j8
-RUN sudo make install
+RUN make install
 WORKDIR /LeanEuclid
 
 # Install smt-portfolio.

From dbf3965d9b6b2a2c917e0f9f9058697eaef6511e Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Wed, 29 May 2024 11:25:16 -0500
Subject: [PATCH 7/9] finish docker

---
 Dockerfile       |  8 ++++----
 scripts/build.sh | 23 +++++++++++++++++++++++
 2 files changed, 27 insertions(+), 4 deletions(-)
 create mode 100644 scripts/build.sh

diff --git a/Dockerfile b/Dockerfile
index b8885d9..7356d6c 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -24,9 +24,10 @@ RUN make -j8
 RUN make install
 WORKDIR /LeanEuclid
 
-# Install smt-portfolio.
-RUN pip3 install --upgrade pip
-RUN pip3 install smt-portfolio
+# Install smt-portfolio in venv.
+RUN python3 -m venv venv
+RUN venv/bin/pip install smt-portfolio
+ENV PATH="/LeanEuclid/venv/bin:${PATH}"
 
 # Install elan.
 ENV ELAN_HOME="/.elan"
@@ -37,4 +38,3 @@ RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -
 RUN lake script run check
 RUN lake exe cache get
 RUN lake build SystemE Book UniGeo E3
-RUN lake -R -Kenv=dev build SystemE:docs
diff --git a/scripts/build.sh b/scripts/build.sh
new file mode 100644
index 0000000..9622d01
--- /dev/null
+++ b/scripts/build.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+
+# Install elan.
+curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
+source $HOME/.elan/env
+
+# Build and Install CVC5.
+git clone https://github.com/cvc5/cvc5 && cd cvc5
+./configure.sh --auto-download
+cd build && make -j8 && sudo make install
+cd ../..
+
+# Build and Install Z3.
+git clone https://github.com/Z3Prover/z3 && cd z3
+python3 scripts/mk_make.py
+cd build && make -j8 && sudo make install
+cd ../..
+
+pip install smt-portfolio
+
+lake script run check
+lake exe cache get
+lake build SystemE Book UniGeo E3
\ No newline at end of file

From 766163ef65f52b0bb17e81089f6132b86f879735 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Wed, 29 May 2024 11:31:24 -0500
Subject: [PATCH 8/9] minor edits

---
 AutoFormalization/proof/autoformalize.py |  4 +-
 AutoFormalization/statement/evaluate.py  | 12 ++--
 E3/Engine/choosePerms.py                 | 91 +++++++++++++++++-------
 README.md                                |  2 +
 scripts/build.sh                         |  2 +
 5 files changed, 75 insertions(+), 36 deletions(-)

diff --git a/AutoFormalization/proof/autoformalize.py b/AutoFormalization/proof/autoformalize.py
index d435532..4238ab6 100644
--- a/AutoFormalization/proof/autoformalize.py
+++ b/AutoFormalization/proof/autoformalize.py
@@ -10,7 +10,9 @@
 
 
 def preceding_propositions(idx):
-    with open("AutoFormalization/proof/book_propositions.json", "r", encoding="utf-8") as f:
+    with open(
+        "AutoFormalization/proof/book_propositions.json", "r", encoding="utf-8"
+    ) as f:
         propositions = json.load(f)
     pre_props = []
     for i in range(1, idx):
diff --git a/AutoFormalization/statement/evaluate.py b/AutoFormalization/statement/evaluate.py
index a54417e..2a6ed68 100644
--- a/AutoFormalization/statement/evaluate.py
+++ b/AutoFormalization/statement/evaluate.py
@@ -6,6 +6,7 @@
 from E3.checker import Checker
 from E3.utils import ROOT_DIR
 
+
 def main():
     parser = argparse.ArgumentParser()
     parser.add_argument(
@@ -32,14 +33,9 @@ def main():
     )
     parser.add_argument(
         "--mode",
-        choices=[
-            "bvars", 
-            "skipApprox", 
-            "onlyApprox", 
-            "full"
-        ],
+        choices=["bvars", "skipApprox", "onlyApprox", "full"],
         default="skipApprox",
-        help="E3 checker mode"
+        help="E3 checker mode",
     )
     parser.add_argument(
         "--reasoning",
@@ -112,7 +108,7 @@ def main():
                         cnt += 1
                 except Exception as e:
                     print(e)
-                    continue 
+                    continue
 
     print(f"cnt: {cnt}, tot: {tot}, acc: {(cnt/tot)*100:.2f}%")
 
diff --git a/E3/Engine/choosePerms.py b/E3/Engine/choosePerms.py
index b5f44ac..a56a0b3 100644
--- a/E3/Engine/choosePerms.py
+++ b/E3/Engine/choosePerms.py
@@ -6,13 +6,16 @@
 from dataclasses import dataclass, field
 from collections import Counter
 
+
 def is_permutation(list1, list2):
     return Counter(list1) == Counter(list2)
 
+
 SHORTCIRCUIT_THRESHOLD = 4000000
 SHORTCIRCUIT_SAMPLE_THRESHOLD = 0.88
 SHORTCIRCUIT_SAMPLE_CUTOFF = 50
 
+
 class QuantifierData:
     points: list[str]
     lines: list[str]
@@ -23,8 +26,14 @@ def __init__(self, points, lines, circles):
         self.lines = lines
         self.circles = circles
 
-def has_permutation(x:QuantifierData,y:QuantifierData):
-    return is_permutation(x.points, y.points) and is_permutation(x.lines, y.lines) and is_permutation (x.circles, y.circles)
+
+def has_permutation(x: QuantifierData, y: QuantifierData):
+    return (
+        is_permutation(x.points, y.points)
+        and is_permutation(x.lines, y.lines)
+        and is_permutation(x.circles, y.circles)
+    )
+
 
 class PropData:
     univNames: QuantifierData
@@ -33,12 +42,22 @@ class PropData:
     def __init__(self, univNames, existNames):
         self.univNames = univNames
         self.existNames = existNames
-    
-    def asList(self):
-        return self.univNames.points + self.univNames.lines + self.univNames.circles + self.existNames.points + self.existNames.lines + self.existNames.circles
 
-def has_match(x : PropData, y : PropData):
-    return has_permutation(x.univNames,y.univNames) and has_permutation(x.existNames, y.existNames)
+    def asList(self):
+        return (
+            self.univNames.points
+            + self.univNames.lines
+            + self.univNames.circles
+            + self.existNames.points
+            + self.existNames.lines
+            + self.existNames.circles
+        )
+
+
+def has_match(x: PropData, y: PropData):
+    return has_permutation(x.univNames, y.univNames) and has_permutation(
+        x.existNames, y.existNames
+    )
 
 
 class PermutationStruct:
@@ -75,7 +94,7 @@ class NameMap:
     sim: float
 
     def __eq__(self, other) -> bool:
-        self.name==other.name
+        self.name == other.name
 
 
 def readNames(data):
@@ -115,7 +134,8 @@ def checkPerm(names, target, reference, guarded):
 
 
 def checkAndInsert(heap, name, N):
-    if name in heap: return ()
+    if name in heap:
+        return ()
     if len(heap) < N:
         heapq.heappush(heap, name)
     else:
@@ -155,24 +175,30 @@ def choosePermutations(
 
     nonempty_names = []
 
-
-    if not univ.noPoints(): nonempty_names+=[univ.pointPerms]
-    if not univ.noLines(): nonempty_names+=[univ.linePerms]
-    if not univ.noCircles(): nonempty_names+=[univ.circlePerms]
-    if not exist.noPoints(): nonempty_names+=[exist.pointPerms]
-    if not exist.noLines(): nonempty_names+=[exist.linePerms]
-    if not exist.noCircles(): nonempty_names+=[exist.circlePerms]
-
+    if not univ.noPoints():
+        nonempty_names += [univ.pointPerms]
+    if not univ.noLines():
+        nonempty_names += [univ.linePerms]
+    if not univ.noCircles():
+        nonempty_names += [univ.circlePerms]
+    if not exist.noPoints():
+        nonempty_names += [exist.pointPerms]
+    if not exist.noLines():
+        nonempty_names += [exist.linePerms]
+    if not exist.noCircles():
+        nonempty_names += [exist.circlePerms]
 
     ceiling = 1
     for x in nonempty_names:
         ceiling *= ceiling * len(x)
-    if ceiling > SHORTCIRCUIT_THRESHOLD :
+    if ceiling > SHORTCIRCUIT_THRESHOLD:
         short_circuiting = True
 
-    if has_match(ground,remove_all_guards(test)):
+    if has_match(ground, remove_all_guards(test)):
         print("match found")
-        sim = checkPerm(ground.asList(), target, reference, replaceGuards(ground.asList()))
+        sim = checkPerm(
+            ground.asList(), target, reference, replaceGuards(ground.asList())
+        )
         checkAndInsert(permHeap, NameMap(ground.asList(), sim), N)
 
     for uPoints, uLines, uCircles, ePoints, eLines, eCircles in allCombs:
@@ -180,9 +206,9 @@ def choosePermutations(
         sim = checkPerm(asList, target, reference, perm)
         x = NameMap(perm, sim)
         checkAndInsert(permHeap, x, N)
-        if (short_circuiting and sim > SHORTCIRCUIT_SAMPLE_THRESHOLD):
+        if short_circuiting and sim > SHORTCIRCUIT_SAMPLE_THRESHOLD:
             seen_sc += 1
-        if (short_circuiting and seen_sc >= SHORTCIRCUIT_SAMPLE_CUTOFF):
+        if short_circuiting and seen_sc >= SHORTCIRCUIT_SAMPLE_CUTOFF:
             return permHeap, asList
     return permHeap, asList
 
@@ -190,13 +216,24 @@ def choosePermutations(
 def removeGuards(data):
     return list(map(lambda x: x.replace("grd_", ""), data))
 
+
 def replaceGuards(data):
-    return list(map(lambda x : "grd_"+x,data))
+    return list(map(lambda x: "grd_" + x, data))
+
 
 def remove_all_guards(x: PropData):
-    univ = QuantifierData(removeGuards(x.univNames.points), removeGuards(x.univNames.lines), removeGuards(x.univNames.circles))
-    exist = QuantifierData(removeGuards(x.existNames.points), removeGuards(x.existNames.lines), removeGuards(x.existNames.circles))
-    return PropData(univ,exist)
+    univ = QuantifierData(
+        removeGuards(x.univNames.points),
+        removeGuards(x.univNames.lines),
+        removeGuards(x.univNames.circles),
+    )
+    exist = QuantifierData(
+        removeGuards(x.existNames.points),
+        removeGuards(x.existNames.lines),
+        removeGuards(x.existNames.circles),
+    )
+    return PropData(univ, exist)
+
 
 def main():
 
@@ -229,6 +266,6 @@ def main():
     with open(args.outFile, "w") as file:
         json.dump(dict, file)
 
+
 if __name__ == "__main__":
     main()
-
diff --git a/README.md b/README.md
index 5e92cea..a15d6eb 100644
--- a/README.md
+++ b/README.md
@@ -67,6 +67,8 @@ Optionally, you can:
 1. Run `lake -R -Kenv=dev build SystemE:docs` to build the documentation
 1. View the auto-generated documentation locally at ./lake/build/doc, e.g., using `python -mhttp.server`
 
+If you have problems building the project, [Dockerfile](./Dockerfile) and [scripts/build.sh](./scripts/build.sh) may serve as useful references.
+
 
 ## The Formal System E
 
diff --git a/scripts/build.sh b/scripts/build.sh
index 9622d01..52c19a7 100644
--- a/scripts/build.sh
+++ b/scripts/build.sh
@@ -1,4 +1,5 @@
 #!/bin/bash
+# This script was designed to run on GitHub Codespaces.
 
 # Install elan.
 curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
@@ -18,6 +19,7 @@ cd ../..
 
 pip install smt-portfolio
 
+# Build the Lean project.
 lake script run check
 lake exe cache get
 lake build SystemE Book UniGeo E3
\ No newline at end of file

From 2628d91b76eff699f2dff2a033ae9c199076e0d7 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Wed, 29 May 2024 11:44:19 -0500
Subject: [PATCH 9/9] remove All.lean

---
 .gitignore    |    1 +
 Book/All.lean | 1388 -------------------------------------------------
 2 files changed, 1 insertion(+), 1388 deletions(-)
 delete mode 100644 Book/All.lean

diff --git a/.gitignore b/.gitignore
index 6783599..1cdcc6e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
+Book/All.lean
 /build
 /lake-packages/*
 /.lake/*
diff --git a/Book/All.lean b/Book/All.lean
deleted file mode 100644
index 6a91a1b..0000000
--- a/Book/All.lean
+++ /dev/null
@@ -1,1388 +0,0 @@
-import SystemE
-
-namespace Elements
-
-theorem proposition_1 : ∀ (a b : Point) (AB : Line),
-  distinctPointsOnLine a b AB →
-  ∃ c : Point, |(c─a)| = |(a─b)| ∧ |(c─b)| = |(a─b)| :=
-by
-  euclid_intros
-  euclid_apply circle_from_points a b as BCD
-  euclid_apply circle_from_points b a as ACE
-  euclid_apply intersection_circles BCD ACE as c
-  euclid_apply point_on_circle_onlyif a b c BCD
-  euclid_apply point_on_circle_onlyif b a c ACE
-  use c
-  euclid_finish
-
-theorem proposition_1' : ∀ (a b x : Point) (AB : Line),
-  distinctPointsOnLine a b AB ∧ ¬(x.onLine AB) →
-  ∃ c : Point, |(c─a)| = |(a─b)| ∧ |(c─b)| = |(a─b)| ∧ (c.opposingSides x AB) :=
-by
-  euclid_intros
-  euclid_apply circle_from_points a b as BCD
-  euclid_apply circle_from_points b a as ACE
-  euclid_apply intersection_opposite_side BCD ACE x a b AB as c
-  euclid_apply point_on_circle_onlyif a b c BCD
-  euclid_apply point_on_circle_onlyif b a c ACE
-  use c
-  euclid_finish
-
-theorem proposition_2 : ∀ (a b c : Point) (BC : Line),
-  (distinctPointsOnLine b c BC) ∧ (a ≠ b) →
-  ∃ l : Point, |(a─l)| = |(b─c)| :=
-by
-  euclid_intros
-  euclid_apply (line_from_points a b) as AB
-  euclid_apply (proposition_1 a b AB) as d
-  euclid_apply (line_from_points d a ) as AE
-  euclid_apply (line_from_points d b ) as BF
-  euclid_apply (circle_from_points b c) as CGH
-  euclid_apply (intersection_circle_line_extending_points CGH BF b d) as g
-  euclid_apply (circle_from_points d g) as GKL
-  euclid_apply (intersection_circle_line_extending_points GKL AE a d) as l
-  euclid_apply (point_on_circle_onlyif b c g CGH)
-  euclid_apply (point_on_circle_onlyif d l g GKL)
-  euclid_apply (between_if l a d )
-  euclid_apply (between_if g b d )
-  use l
-  euclid_finish
-
-/-
-An extension of proposition_2 to the case where a and b may be the same point.
--/
-theorem proposition_2' : ∀ (a b c : Point) (BC : Line),
-  distinctPointsOnLine b c BC →
-  ∃ l : Point, |(a─l)| = |(b─c)| :=
-by
-  euclid_intros
-  by_cases (a = b)
-  . use c
-    euclid_finish
-  . euclid_apply proposition_2 a b c BC as l
-    use l
-
-theorem proposition_3 : ∀ (a b c₀ c₁ : Point) (AB C : Line),
-  distinctPointsOnLine a b AB ∧ distinctPointsOnLine c₀ c₁ C ∧ |(a─b)| > |(c₀─c₁)| →
-  ∃ e : Point, between a e b ∧ |(a─e)| = |(c₀─c₁)| :=
-by
-  euclid_intros
-  euclid_apply (proposition_2' a c₀ c₁ C) as d
-  euclid_apply (circle_from_points a d) as DEF
-  euclid_apply (intersection_circle_line_between_points DEF AB a b) as e
-  euclid_apply (point_on_circle_onlyif a d e)
-  use e
-  euclid_finish
-
-theorem proposition_4 : ∀ (a b c d e f : Point) (AB BC AC DE EF DF : Line),
-  formTriangle a b c AB BC AC ∧ formTriangle d e f DE EF DF ∧
-  |(a─b)| = |(d─e)| ∧ |(a─c)| = |(d─f)| ∧ (∠ b:a:c = ∠ e:d:f) →
-  |(b─c)| = |(e─f)| ∧ (∠ a:b:c = ∠ d:e:f) ∧ (∠ a:c:b = ∠ d:f:e) :=
-by
-  euclid_intros
-  euclid_apply (superposition a b c d e f AB BC AC DE) as (b', c', BC', DC')
-  euclid_assert b' = e
-  euclid_assert ∠ e:d:c' = ∠ e:d:f
-  euclid_assert DC' = DF
-  euclid_assert c' = f
-  euclid_finish
-
-theorem proposition_5 : ∀ (a b c d e : Point) (AB BC AC : Line),
-  formTriangle a b c AB BC AC ∧ (|(a─b)| = |(a─c)|) ∧
-  (between a b d) ∧ (between a c e) →
-  (∠ a:b:c = ∠ a:c:b) ∧ (∠ c:b:d = ∠ b:c:e) :=
-by
-  euclid_intros
-  euclid_apply (point_between_points_shorter_than AB b d (c─e)) as f
-  euclid_apply (proposition_3 a e f a AC AB) as g
-  euclid_apply (line_from_points c f) as FC
-  euclid_apply (line_from_points b g) as GB
-  euclid_apply (proposition_4 a f c a g b AB FC AC AC GB AB)
-  euclid_apply (proposition_4 f b c g c b AB BC FC AC BC GB)
-  euclid_apply (sum_angles_onlyif b a g c AB GB)
-  euclid_apply (sum_angles_onlyif c a f b AC FC)
-  euclid_finish
-
-/--
-A restriction of proposition_5.
--/
-theorem proposition_5' : ∀ (a b c : Point) (AB BC AC : Line),
-  formTriangle a b c AB BC AC ∧ (|(a─b)| = |(a─c)|) →
-  (∠ a:b:c = ∠ a:c:b) :=
-by
-  euclid_intros
-  euclid_apply (extend_point AB a b) as d
-  euclid_apply (extend_point AC a c) as e
-  euclid_apply (proposition_5 a b c d e AB BC AC)
-  euclid_finish
-
-theorem proposition_6 : ∀ (a b c : Point) (AB BC AC : Line),
-  formTriangle a b c AB BC AC ∧ (∠ a:b:c = ∠ a:c:b) →
-  |(a─b)| = |(a─c)| :=
-by
-  euclid_intros
-  by_contra
-  by_cases |(a─b)| > |(a─c)|
-  . euclid_apply (proposition_3 b a a c AB AC) as d
-    euclid_apply (line_from_points d c) as DC
-    euclid_apply proposition_4 b d c c a b AB DC BC AC AB BC
-    euclid_finish
-  . euclid_apply (proposition_3 c a a b AC AB) as d
-    euclid_apply (line_from_points d b) as DB
-    euclid_apply (proposition_4 c d b b a c AC DB BC AB AC BC)
-    euclid_finish
-
-theorem proposition_7 : ∀ (a b c d : Point) (AB AC CB AD DB : Line),
-  distinctPointsOnLine a b AB ∧ distinctPointsOnLine a c AC ∧ distinctPointsOnLine c b CB ∧
-  distinctPointsOnLine a d AD ∧ distinctPointsOnLine d b DB ∧ (c.sameSide d AB) ∧ c ≠ d ∧
-  (|(a─c)| = |(a─d)|) ∧ (|(c─b)| = |(d─b)|) → False :=
-by
-  euclid_intros
-  euclid_apply (line_from_points c d) as CD
-  by_cases a.sameSide b CD <;> by_cases d.sameSide b AC
-  · euclid_apply (proposition_5' a c d AC CD AD)
-    euclid_apply (sum_angles_onlyif d c b a CD DB)
-    euclid_apply (proposition_5' b c d CB CD DB)
-    euclid_apply (sum_angles_onlyif c a d b AC CD)
-    euclid_finish
-  · -- Omitted by Euclid.
-    euclid_apply (proposition_5' a d c AD CD AC)
-    euclid_apply (sum_angles_onlyif c d b a CD CB)
-    euclid_apply (proposition_5' b d c DB CD CB)
-    euclid_apply (sum_angles_onlyif d a c b AD CD)
-    euclid_finish
-  · -- Omitted by Euclid.
-    euclid_apply (extend_point AC a c) as e
-    euclid_apply (extend_point AD a d) as f
-    euclid_apply (proposition_5 a c d e f AC CD AD)
-    euclid_apply (sum_angles_onlyif c e d b AC CD)
-    euclid_apply (proposition_5' b c d CB CD DB)
-    euclid_apply (sum_angles_onlyif d c b f CD DB)
-    euclid_finish
-  · -- Omitted by Euclid.
-    euclid_apply (extend_point AC a c) as e
-    euclid_apply (extend_point AD a d) as f
-    euclid_apply (proposition_5 a c d e f AC CD AD)
-    euclid_apply (sum_angles_onlyif d f c b AD CD)
-    euclid_apply (proposition_5' b d c DB CD CB)
-    euclid_apply (sum_angles_onlyif c d b e CD CB)
-    euclid_finish
-
-theorem proposition_8 : ∀ (a b c d e f : Point) (AB BC AC DE EF DF : Line),
-  formTriangle a b c AB BC AC ∧ formTriangle d e f DE EF DF ∧
-  |(a─b)| = |(d─e)| ∧ |(a─c)| = |(d─f)| ∧ |(b─c)| = |(e─f)| →
-  ∠ b:a:c = ∠ e:d:f :=
-by
-    euclid_intros
-    euclid_apply (superposition b c a e f d BC AC AB EF) as (c', g, CG', EG)
-    euclid_assert c' = f
-    by_cases d = g
-    · euclid_finish
-    · euclid_apply (proposition_7 e f d g EF DE DF EG CG')
-      euclid_finish
-
-theorem proposition_9 : ∀ (a b c : Point) (AB AC : Line),
-  formRectilinearAngle b a c AB AC ∧ AB ≠ AC →
-  ∃ f : Point, f ≠ a ∧ (∠ b:a:f = ∠ c:a:f) :=
-by
-  euclid_intros
-  euclid_apply point_between_points_shorter_than AB a b (a─c) as d
-  euclid_apply (proposition_3 a c a d AC AB) as e
-  euclid_apply (line_from_points d e) as DE
-  euclid_apply (proposition_1' d e a DE) as f
-  euclid_apply (line_from_points f e) as FE
-  euclid_apply (line_from_points f d) as FD
-  euclid_apply (line_from_points a f) as AF
-  use f
-  have : ¬(f.onLine AB) := by  -- Omitted by Euclid.
-    euclid_intros
-    euclid_apply (proposition_5' f d e AB DE FE)
-    euclid_apply (proposition_5 a d e b c AB DE AC)
-    euclid_finish
-  have : ¬(f.onLine AC) := by  -- Omitted by Euclid.
-    euclid_intros
-    euclid_apply (proposition_5' f e d AC DE FD)
-    euclid_apply (proposition_5 a d e b c AB DE AC)
-    euclid_finish
-  euclid_apply (proposition_8 a d f a e f AB FD AF AC FE AF)
-  euclid_finish
-
-theorem proposition_9' : ∀ (a b c : Point) (AB AC : Line),
-  formRectilinearAngle b a c AB AC ∧ AB ≠ AC →
-  ∃ f : Point, (f.sameSide c AB) ∧ (f.sameSide b AC) ∧ (∠ b:a:f = ∠ c:a:f) :=
-by
-  euclid_intros
-  euclid_apply (point_between_points_shorter_than AB a b (a─c)) as d
-  euclid_apply (proposition_3 a c a d AC AB) as e
-  euclid_apply (line_from_points d e) as DE
-  euclid_apply (proposition_1' d e a DE) as f
-  euclid_apply (line_from_points f e) as FE
-  euclid_apply (line_from_points f d) as FD
-  euclid_apply (line_from_points a f) as AF
-  use f
-  have : ¬(f.onLine AB) := by  -- Omitted by Euclid.
-    euclid_intros
-    euclid_apply (proposition_5' f d e AB DE FE)
-    euclid_apply (proposition_5 a d e b c AB DE AC)
-    euclid_finish
-  have : ¬(f.onLine AC) := by  -- Omitted by Euclid.
-    euclid_intros
-    euclid_apply (proposition_5' f e d AC DE FD)
-    euclid_apply (proposition_5 a d e b c AB DE AC)
-    euclid_finish
-  euclid_apply (proposition_8 a d f a e f AB FD AF AC FE AF)
-  euclid_apply (intersection_lines AF DE) as g
-  euclid_finish
-
-theorem proposition_10 : ∀ (a b : Point) (AB : Line), distinctPointsOnLine a b AB →
-  ∃ d : Point, (between a d b) ∧ (|(a─d)| = |(d─b)|) :=
-by
-  euclid_intros
-  euclid_apply (proposition_1 a b AB) as c
-  euclid_apply (line_from_points c a) as AC
-  euclid_apply (line_from_points c b ) as BC
-  euclid_apply (proposition_9' c a b AC BC) as d'
-  euclid_apply (line_from_points c d') as CD
-  euclid_apply (intersection_lines CD AB) as d
-  euclid_apply (proposition_4 c a d c b d AC AB CD BC AB CD)
-  use d
-  euclid_finish
-
-theorem proposition_11 : ∀ (a b c : Point) (AB : Line),
-  distinctPointsOnLine a b AB ∧ between a c b →
-  exists f : Point, ¬(f.onLine AB) ∧ (∠ a:c:f = ∟) :=
-by
-  euclid_intros
-  euclid_apply (point_between_points_shorter_than AB c a (c─b)) as d
-  euclid_apply (proposition_3 c b c d AB AB) as e
-  euclid_apply (proposition_1 d e AB) as f
-  euclid_apply (line_from_points d f) as DF
-  euclid_apply (line_from_points f e) as FE
-  euclid_apply (line_from_points f c) as FC
-  euclid_apply (proposition_8 c d f c e f AB DF FC AB FE FC)
-  euclid_apply (perpendicular_if d e c f AB)
-  use f
-  euclid_finish
-
-theorem proposition_11' : ∀ (a b c x : Point) (AB : Line),
-  (distinctPointsOnLine a b AB) ∧ (between a c b) ∧ ¬(x.onLine AB) →
-  exists f : Point, (f.sameSide x AB) ∧ (∠ a:c:f = ∟) :=
-by
-  euclid_intros
-  euclid_apply (point_between_points_shorter_than AB c a (c─b)) as d
-  euclid_apply (proposition_3 c b c d AB AB) as e
-  euclid_apply (exists_point_opposite AB x) as h
-  euclid_apply (proposition_1' d e h AB) as f
-  euclid_apply (line_from_points d f) as DF
-  euclid_apply (line_from_points f e) as FE
-  euclid_apply (line_from_points f c) as FC
-  euclid_apply (proposition_8 c d f c e f AB DF FC AB FE FC)
-  euclid_apply (perpendicular_if d e c f AB)
-  use f
-  euclid_finish
-
-theorem proposition_11'' : ∀ (a b : Point) (AB : Line),
-  distinctPointsOnLine a b AB →
-  exists (f : Point), ¬(f.onLine AB) ∧ (∠ f:a:b = ∟) :=
-by
-  euclid_intros
-  euclid_apply (extend_point AB b a) as c
-  euclid_apply (proposition_11 c b a AB) as f
-  use f
-  euclid_finish
-
-theorem proposition_11''' : ∀ (a b x : Point) (AB : Line),
-  ¬(x.onLine AB) ∧ (distinctPointsOnLine a b AB) →
-  exists (f : Point), ¬(f.onLine AB) ∧ (f.opposingSides x AB) ∧ (∠ f:a:b = ∟) :=
-by
-  euclid_intros
-  euclid_apply (extend_point AB b a) as c
-  euclid_apply (exists_point_opposite AB x) as g
-  euclid_apply (proposition_11' c b a g AB) as f
-  use f
-  euclid_finish
-
-theorem proposition_12 : ∀ (a b c : Point) (AB : Line),
-  distinctPointsOnLine a b AB ∧ ¬(c.onLine AB) →
-  exists h : Point, h.onLine AB ∧ (∠ a:h:c = ∟ ∨ ∠ b:h:c = ∟) :=
-by
-  euclid_intros
-  euclid_apply (exists_point_opposite AB c) as d
-  euclid_apply (circle_from_points c d) as EFG
-  euclid_apply (intersections_circle_line EFG AB) as (e, g)
-  euclid_apply (proposition_10 e g AB) as h
-  euclid_apply (line_from_points c g) as CG
-  euclid_apply (line_from_points c h) as CH
-  euclid_apply (line_from_points c e) as CE
-  use h
-  euclid_apply (proposition_8 h c g h c e CH CG AB CH CE AB)
-  euclid_finish
-
-theorem proposition_13 : ∀ (a b c d : Point) (AB CD : Line),
-  AB ≠ CD ∧ distinctPointsOnLine a b AB ∧ distinctPointsOnLine c d CD ∧ between d b c →
-  ∠ c:b:a + ∠ a:b:d = ∟ + ∟ :=
-by
-  euclid_intros
-  by_cases ∠ c:b:a = ∠ a:b:d
-  . euclid_finish
-  . euclid_apply (proposition_11' d c b a CD) as e
-    euclid_apply (line_from_points b e) as BE
-    euclid_finish
-
-theorem proposition_14 : ∀ (a b c d : Point) (AB BC BD : Line),
-  distinctPointsOnLine a b AB ∧ distinctPointsOnLine b c BC ∧ distinctPointsOnLine b d BD ∧ (c.opposingSides d AB) ∧
-  (∠ a:b:c + ∠ a:b:d) = ∟ + ∟ →
-  BC = BD :=
-by
-  euclid_intros
-  by_contra
-  euclid_apply (extend_point BC c b) as e
-  euclid_apply (proposition_13 a b e c AB BC)
-  by_cases a.sameSide e BD
-  . euclid_apply (sum_angles_onlyif b a d e AB BD)
-    euclid_finish
-  . -- Omitted by Euclid.
-    euclid_apply (sum_angles_onlyif b a e d AB BC)
-    euclid_finish
-
-theorem proposition_15 : ∀ (a b c d e : Point) (AB CD : Line),
-  distinctPointsOnLine a b AB ∧ distinctPointsOnLine c d CD ∧ e.onLine AB ∧ e.onLine CD ∧
-  CD ≠ AB ∧ (between d e c) ∧ (between a e b) →
-  (∠ a:e:c = ∠ d:e:b) ∧ (∠ c:e:b = ∠ a:e:d) :=
-by
-   euclid_intros
-   euclid_apply (proposition_13 a e c d AB CD)
-   euclid_apply (proposition_13 d e a b CD AB)
-   euclid_apply (proposition_13 c e a b CD AB)
-   euclid_finish
-
-theorem proposition_16 : ∀ (a b c d : Point) (AB BC AC: Line),
-  formTriangle a b c AB BC AC ∧ (between b c d) →
-  (∠ a:c:d > ∠ c:b:a) ∧ (∠ a:c:d > ∠ b:a:c) :=
-by
-  euclid_intros
-  constructor
-  · -- Omitted by Euclid.
-    euclid_apply (proposition_10 b c BC) as e
-    euclid_apply (line_from_points a e) as AE
-    euclid_apply (extend_point_longer AE a e (a─e)) as f'
-    euclid_apply (proposition_3 e f' a e AE AE) as f
-    euclid_apply (line_from_points f c) as FC
-    euclid_apply (proposition_15 b c a f e BC AE)
-    euclid_apply (proposition_4 e b a e c f BC AB AE BC FC AE)
-    euclid_apply (extend_point AC a c) as g
-    euclid_apply (proposition_15 a g b d c AC BC)
-    euclid_finish
-  · euclid_apply (proposition_10 a c AC) as e
-    euclid_apply (line_from_points b e) as BE
-    euclid_apply (extend_point_longer BE b e (b─e)) as f'
-    euclid_apply (proposition_3 e f' b e BE BE) as f
-    euclid_apply (line_from_points f c) as FC
-    euclid_apply (proposition_15 a c b f e AC BE)
-    euclid_apply (proposition_4 e b a e f c BE AB AC BE FC AC)
-    euclid_finish
-
-theorem proposition_17 : ∀ (a b c : Point) (AB BC AC : Line),
-  formTriangle a b c AB BC AC →
-  ∠ a:b:c + ∠ b:c:a < ∟ + ∟ :=
-by
-  euclid_intros
-  euclid_apply (extend_point BC b c) as d
-  euclid_apply (proposition_16 a b c d AB BC AC)
-  euclid_apply (proposition_13 a c b d AC BC)
-  euclid_finish
-
-theorem proposition_18 : ∀ (a b c : Point) (AB BC AC : Line),
-  formTriangle a b c AB BC AC ∧ (|(a─c)| > |(a─b)|) →
-  (∠ a:b:c > ∠ b:c:a) :=
-by
-  euclid_intros
-  euclid_apply (proposition_3 a c a b AC AB) as d
-  euclid_apply (line_from_points b d) as BD
-  euclid_apply (proposition_16 b c d a BC AC BD)
-  euclid_apply (proposition_5' a b d AB BD AC)
-  euclid_apply (sum_angles_if b a c d AB BC)
-  euclid_finish
-
-theorem proposition_19 : ∀ (a b c : Point) (AB BC AC : Line),
-  formTriangle a b c AB BC AC ∧ (∠ a:b:c > ∠ b:c:a) →
-  (|(a─c)| > |(a─b)|) :=
-by
-  euclid_intros
-  by_contra
-  by_cases |(a─c)| = |(a─b)|
-  . euclid_apply (proposition_5' a b c AB BC AC)
-    euclid_finish
-  . euclid_apply (proposition_18 a c b AC BC AB)
-    euclid_finish
-
-theorem proposition_20 : ∀ (a b c : Point) (AB BC AC : Line),
-  formTriangle a b c AB BC AC → |(b─a)| + |(a─c)| > |(b─c)| :=
-by
-  euclid_intros
-  euclid_apply (extend_point_longer AB b a (c─a)) as d'
-  euclid_apply (proposition_3 a d' a c AB AC) as d
-  euclid_apply (line_from_points d c) as DC
-  euclid_apply (proposition_5' a c d AC DC AB)
-  euclid_apply (sum_angles_onlyif c b d a BC DC)
-  euclid_apply (proposition_19 b c d BC DC AB)
-  euclid_finish
-
-theorem proposition_21 : ∀ (a b c d : Point) (AB BC AC BD DC : Line),
-  formTriangle a b c AB BC AC ∧ (a.sameSide d BC) ∧ (c.sameSide d AB) ∧ (b.sameSide d AC) ∧
-  distinctPointsOnLine b d BD ∧ distinctPointsOnLine d c DC →
-  (|(b─d)| + |(d─c)| < |(b─a)| + |(a─c)|) ∧ (∠ b:d:c > ∠ b:a:c) :=
-by
-  euclid_intros
-  euclid_apply (intersection_lines BD AC) as e
-  euclid_apply (proposition_20 a b e AB BD AC)
-  euclid_apply (proposition_20 e d c BD DC AC)
-  constructor
-  . euclid_finish
-  . euclid_apply (proposition_16 c e d b AC BD DC)
-    euclid_apply (proposition_16 b a e c AB AC BD)
-    euclid_finish
-
-theorem proposition_22 : ∀ (a a' b b' c c' : Point) (A B C : Line),
-  distinctPointsOnLine a a' A ∧ distinctPointsOnLine b b' B ∧ distinctPointsOnLine c c' C ∧
-  (|(a─a')| + |(b─b')| > |(c─c')|) ∧
-  (|(a─a')| + |(c─c')| > |(b─b')|) ∧
-  (|(b─b')| + |(c─c')| > |(a─a')|) →
-  ∃ (k f g : Point), (|(f─k)| = |(a─a')|) ∧ (|(f─g)| = |(b─b')|) ∧ (|(k─g)| = |(c─c')|) :=
-by
-  euclid_intros
-  euclid_apply arbitrary_point as d
-  euclid_apply (distinct_points d) as e'
-  euclid_apply (line_from_points d e') as DE
-  euclid_apply (extend_point_longer DE d e' (a─a')) as e''
-  euclid_apply (extend_point_longer DE d e'' (b─b')) as e'''
-  euclid_apply (extend_point_longer DE d e''' (c─c')) as e
-  euclid_apply (proposition_3 d e a a' DE A ) as f
-  euclid_apply (proposition_3 f e b b' DE B) as g
-  euclid_apply (proposition_3 g e c c' DE C) as h
-  euclid_apply (circle_from_points f d) as DKL
-  euclid_apply (circle_from_points g h) as KLH
-  -- Euclid didn't need to explicitly note the existence of i.
-  euclid_apply (intersection_circle_line_extending_points KLH DE g h) as i
-  euclid_apply (intersection_circles KLH DKL) as k
-  use k, f, g
-  euclid_apply (point_on_circle_onlyif f d k DKL)
-  euclid_apply (point_on_circle_onlyif g k h KLH)
-  euclid_finish
-
--- An extension of proposition 22 given a line and two points on it.
-theorem proposition_22' : ∀ (a a' b b' c c' f e : Point) (A B C FE : Line),
-  distinctPointsOnLine a a' A ∧ distinctPointsOnLine b b' B ∧ distinctPointsOnLine c c' C ∧ distinctPointsOnLine f e FE ∧
-  (|(a─a')| + |(b─b')| > |(c─c')|) ∧
-  (|(a─a')| + |(c─c')| > |(b─b')|) ∧
-  (|(b─b')| + |(c─c')| > |(a─a')|) →
-  ∃ (k g : Point), g.onLine FE ∧ ¬(between g f e) ∧
-  (|(f─k)| = |(a─a')|) ∧ (|(f─g)| = |(b─b')|) ∧ (|(k─g)| = |(c─c')|) :=
-by
-  euclid_intros
-  euclid_apply (extend_point_longer FE f e (b─b')) as e'
-  euclid_apply (extend_point_longer FE f e' (c─c')) as e''
-  euclid_apply (proposition_3 f e'' a a' FE A) as d
-  euclid_apply (proposition_3 f e'' b b' FE B) as g
-  euclid_apply (proposition_3 g e'' c c' FE C) as h
-  euclid_apply (circle_from_points f d) as DKL
-  euclid_apply (circle_from_points g h) as KLH
-  -- Euclid didn't need to explicitly note the existence of i.
-  euclid_apply (intersection_circle_line_extending_points KLH FE g h) as i
-  euclid_apply (intersection_circles KLH DKL) as k
-  use k, g
-  euclid_apply (point_on_circle_onlyif f d k DKL)
-  euclid_apply (point_on_circle_onlyif g k h KLH)
-  euclid_finish
-
-theorem proposition_22'' : ∀ (a a' b b' c c' f e x : Point) (A B C FE : Line),
-  distinctPointsOnLine a a' A ∧ distinctPointsOnLine b b' B ∧ distinctPointsOnLine c c' C ∧ distinctPointsOnLine f e FE ∧ ¬(x.onLine FE) ∧
-  (|(a─a')| + |(b─b')| > |(c─c')|) ∧
-  (|(a─a')| + |(c─c')| > |(b─b')|) ∧
-  (|(b─b')| + |(c─c')| > |(a─a')|) →
-  ∃ (k g : Point), g.onLine FE ∧ ¬(between g f e) ∧ (k.sameSide x FE) ∧
-  (|(f─k)| = |(a─a')|) ∧ (|(f─g)| = |(b─b')|) ∧ (|(k─g)| = |(c─c')|) :=
-by
-  euclid_intros
-  euclid_apply (extend_point_longer FE f e (b─b')) as e'
-  euclid_apply (extend_point_longer FE f e' (c─c')) as e''
-  euclid_apply (proposition_3 f e'' a a' FE A) as d
-  euclid_apply (proposition_3 f e'' b b' FE B) as g
-  euclid_apply (proposition_3 g e'' c c' FE C) as h
-  euclid_apply (circle_from_points f d) as DKL
-  euclid_apply (circle_from_points g h) as KLH
-  -- Euclid didn't need to explicitly note the existence of i.
-  euclid_apply (intersection_circle_line_extending_points KLH FE g h) as i
-  euclid_apply (intersection_same_side KLH DKL x g f FE) as k
-  use k, g
-  euclid_apply (point_on_circle_onlyif f d k DKL)
-  euclid_apply (point_on_circle_onlyif g k h KLH)
-  euclid_finish
-
-theorem proposition_23 : ∀ (a b c d e : Point) (AB CD CE : Line),
-  distinctPointsOnLine a b AB ∧ formRectilinearAngle d c e CD CE →
-  ∃ f : Point, f ≠ a ∧ (∠ f:a:b = ∠ d:c:e) :=
-by
-  euclid_intros
-  by_cases (d.onLine CE)
-  · -- Omitted by Euclid.
-    by_cases (∠ d:c:e = 0)
-    · use b
-      euclid_finish
-    · euclid_assert ∠ d:c:e = ∟ + ∟
-      euclid_apply (extend_point AB b a) as b'
-      use b'
-      euclid_finish
-  euclid_apply (line_from_points d e) as DE
-  -- Euclid didn't explicitly apply proposition_20.
-  euclid_apply (proposition_20 c d e CD DE CE)
-  euclid_apply (proposition_20 d e c DE CE CD)
-  euclid_apply (proposition_20 e c d CE CD DE)
-  euclid_apply (proposition_22' c d c e e d a b CD CE DE AB) as (f, g)
-  euclid_apply (line_from_points a f) as FA
-  euclid_apply (line_from_points f g) as FG
-  euclid_apply (proposition_8 c d e a f g CD DE CE FA FG AB)
-  use f
-  euclid_finish
-
--- An extension of proposition_23 that allows the angle to be constructed on either side of AB.
-theorem proposition_23' : ∀ (a b c d e x : Point) (AB CD CE : Line),
-  distinctPointsOnLine a b AB ∧ formRectilinearAngle d c e CD CE ∧ ¬(x.onLine AB) →
-  ∃ f : Point, f ≠ a ∧ (f.onLine AB ∨ f.sameSide x AB) ∧ (∠ f:a:b = ∠ d:c:e) :=
-by
-  euclid_intros
-  by_cases (d.onLine CE)
-  . -- Omitted by Euclid.
-    by_cases (∠ d:c:e = 0)
-    . use b
-      euclid_finish
-    . euclid_assert ∠ d:c:e = ∟ + ∟
-      euclid_apply (extend_point AB b a) as b'
-      use b'
-      euclid_finish
-  euclid_apply (line_from_points d e) as DE
-  -- Euclid didn't explicitly apply proposition_20.
-  euclid_apply (proposition_20 c d e CD DE CE)
-  euclid_apply (proposition_20 d e c DE CE CD)
-  euclid_apply (proposition_20 e c d CE CD DE)
-  euclid_apply (proposition_22'' c d c e e d a b x CD CE DE AB) as (f, g)
-  euclid_apply (line_from_points a f) as AF
-  euclid_apply (line_from_points f g) as FG
-  euclid_apply (proposition_8 c d e a f g CD DE CE AF FG AB)
-  use f
-  euclid_finish
-
-theorem proposition_24 : ∀ (a b c d e f : Point) (AB BC AC DE EF DF : Line),
-  formTriangle a b c AB BC AC ∧ formTriangle d e f DE EF DF ∧
-  (|(a─b)| = |(d─e)|) ∧ (|(a─c)| = |(d─f)|) ∧ (∠ b:a:c > ∠ e:d:f) →
-  |(b─c)| > |(e─f)| :=
-by
-  euclid_intros
-  euclid_apply (proposition_23' d e a b c f DE AB AC) as g'
-  euclid_apply (line_from_points d g') as DG
-  euclid_apply (extend_point_longer DG d g' (a─c)) as g''
-  euclid_apply (proposition_3 d g'' a c DG AC) as g
-  euclid_apply (line_from_points e g) as EG
-  euclid_apply (line_from_points f g) as FG
-  euclid_apply (proposition_4 a b c d e g AB BC AC DE EG DG)
-  euclid_apply (proposition_5' d g f DG FG DF)
-  by_cases (d.sameSide g EF)
-  · euclid_assert (∠ d:f:g > ∠ e:g:f)
-    euclid_assert (∠ e:f:g > ∠ e:g:f)
-    euclid_apply (proposition_19 e f g EF FG EG)
-    euclid_finish
-  · -- Omitted by Euclid.
-    by_cases g.onLine EF
-    · euclid_finish
-    · euclid_apply (extend_point FG g f) as h
-      -- Not clear why these are needed.
-      euclid_assert ¬(g.onLine DF)
-      euclid_assert ¬(e.onLine DF)
-      euclid_assert (g.opposingSides e DF)
-      euclid_assert h.sameSide e DF
-
-      euclid_apply (proposition_13 d f g h DF FG)
-      euclid_apply (proposition_13 e f g h EF FG)
-      euclid_apply (proposition_17 d g e DG EG DE)
-      euclid_apply (proposition_17 d f e DF EF DE)
-      euclid_assert (∠ d:g:e < ∟ + ∟)
-      euclid_assert (∠ d:f:e < ∟ + ∟)
-      euclid_assert (∠ e:f:g + ∠ g:f:d + ∠ d:f:e = ∟ + ∟ + ∟ + ∟)
-      euclid_assert (∠ e:f:g > ∠ e:g:f)
-      euclid_apply (proposition_19 e f g EF FG EG)
-      euclid_finish
-
-theorem proposition_25 : ∀ (a b c d e f : Point) (AB BC AC DE EF DF : Line),
-  formTriangle a b c AB BC AC ∧ formTriangle d e f DE EF DF ∧
-  (|(a─b)| = |(d─e)|) ∧ (|(a─c)| = |(d─f)|) ∧ (|(b─c)| > |(e─f)|) →
-  (∠ b:a:c > ∠ e:d:f) :=
-by
-  euclid_intros
-  by_contra
-  by_cases (∠ b:a:c = ∠ e:d:f)
-  · euclid_apply (proposition_4 a b c d e f AB BC AC DE EF DF)
-    euclid_finish
-  · euclid_assert (∠ b:a:c < ∠ e:d:f)
-    euclid_apply (proposition_24 d e f a b c DE EF DF AB BC AC)
-    euclid_finish
-
-theorem proposition_26 : ∀ (a b c d e f : Point) (AB BC AC DE EF DF : Line),
-  formTriangle a b c AB BC AC ∧ formTriangle d e f DE EF DF ∧
-  (∠ a:b:c = ∠ d:e:f) ∧ (∠ b:c:a = ∠ e:f:d) ∧ (|(b─c)| = |(e─f)| ∨ |(a─b)| = |(d─e)|) →
-  (|(a─b)| = |(d─e)|) ∧ (|(b─c)| = |(e─f)|) ∧ (|(a─c)| = |(d─f)|) ∧ (∠ b:a:c = ∠ e:d:f) :=
-by
-  euclid_intros
-  split_ors
-  · have : (|(a─b)| = |(d─e)|) := by
-      by_contra
-      by_cases (|(a─b)| > |(d─e)|)
-      · euclid_apply (proposition_3 b a e d AB DE) as g
-        euclid_apply (line_from_points g c) as GC
-        euclid_apply (proposition_4 b g c e d f AB GC BC DE DF EF)
-        euclid_finish
-      · -- Omitted by Euclid.
-        euclid_assert (|(d─e)| > |(a─b)|)
-        euclid_apply (proposition_3 e d b a DE AB) as g
-        euclid_apply (line_from_points g f) as GF
-        euclid_apply (proposition_4 e g f b a c DE GF EF AB AC BC)
-        euclid_finish
-    euclid_apply (proposition_4 b a c e d f AB AC BC DE DF EF)
-    euclid_finish
-  · have : (|(b─c)| = |(e─f)|) := by
-      by_contra
-      by_cases (|(b─c)| > |(e─f)|)
-      · euclid_apply (proposition_3 b c e f BC EF) as h
-        euclid_apply (line_from_points a h)  as AH
-        euclid_apply (proposition_4 b a h e d f AB AH BC DE DF EF)
-        euclid_apply (proposition_16 a c h b AC BC AH)
-        euclid_finish
-      · -- Omitted by Euclid.
-        euclid_assert (|(e─f)| > |(b─c)|)
-        euclid_apply (proposition_3 e f b c EF BC) as h
-        euclid_apply (line_from_points d h) as DH
-        euclid_apply (proposition_4 e d h b a c DE DH EF AB AC BC)
-        euclid_apply (proposition_16 d f h e DF EF DH)
-        euclid_finish
-    euclid_apply (proposition_4 b a c e d f AB AC BC DE DF EF)
-    euclid_finish
-
-theorem proposition_27 : ∀ (a d e f : Point) (AE FD EF : Line),
-  distinctPointsOnLine a e AE ∧ distinctPointsOnLine f d FD ∧ distinctPointsOnLine e f EF ∧
-  a.opposingSides d EF ∧ (∠ a:e:f = ∠ e:f:d) →
-  ¬(AE.intersectsLine FD) :=
-by
-  euclid_intros
-  by_contra
-  euclid_apply (extend_point AE a e) as b
-  euclid_apply (intersection_lines AE FD) as g
-  by_cases (g.sameSide b EF)
-  . euclid_apply (proposition_16 f g e a FD AE EF)
-    euclid_finish
-  . -- Omitted by Euclid.
-    euclid_apply (proposition_16 e g f d AE FD EF)
-    euclid_finish
-
-theorem proposition_28 : ∀ (a b c d e f g h : Point) (AB CD EF : Line),
-  distinctPointsOnLine a b AB ∧ distinctPointsOnLine c d CD ∧ distinctPointsOnLine e f EF ∧
-  (between a g b) ∧ (between c h d) ∧ (between e g h) ∧ (between g h f) ∧ (b.sameSide d EF) ∧
-  (∠ e:g:b = ∠ g:h:d ∨ ∠ b:g:h + ∠ g:h:d = ∟ + ∟) →
-  ¬(AB.intersectsLine CD) :=
-by
-  euclid_intros
-  split_ors
-  . euclid_apply (proposition_15 a b e h g AB EF)
-    euclid_apply (proposition_27 a d g h AB CD EF)
-    euclid_finish
-  . euclid_apply (proposition_13 h g a b EF AB)
-    euclid_apply (proposition_27 a d g h AB CD EF)
-    euclid_finish
-
-theorem proposition_29 : ∀ (a b c d e f g h : Point) (AB CD EF : Line),
-  distinctPointsOnLine a b AB ∧ distinctPointsOnLine c d CD ∧ distinctPointsOnLine e f EF ∧
-  (between a g b) ∧ (between c h d) ∧ (between e g h) ∧ (between g h f) ∧ (b.sameSide d EF) ∧ ¬(AB.intersectsLine CD)
-  → ∠ a:g:h = ∠ g:h:d ∧ ∠ e:g:b = ∠ g:h:d ∧ ∠ b:g:h + ∠ g:h:d = ∟ + ∟ :=
-by
-  euclid_intros
-  have : ∠ a:g:h = ∠ g:h:d := by
-    by_contra
-    by_cases ∠ a:g:h > ∠ g:h:d
-    · euclid_assert ∠ a:g:h + ∠ b:g:h > ∠ b:g:h + ∠ g:h:d
-      euclid_apply (proposition_13 h g a b EF AB)
-      euclid_assert ∠ b:g:h + ∠ g:h:d < ∟ + ∟
-      euclid_finish
-    · -- Omitted by Euclid.
-      euclid_assert ∠ a:g:h < ∠ g:h:d
-      euclid_assert ∠ a:g:h + ∠ c:h:g < ∠ g:h:d + ∠ c:h:g
-      euclid_apply (proposition_13 g h c d EF CD)
-      euclid_assert ∠ a:g:h + ∠ c:h:g < ∟ + ∟
-      euclid_finish
-
-  euclid_apply (proposition_15 a b e h g AB EF)
-  euclid_apply (proposition_13 b g e h AB EF)
-  euclid_finish
-
-theorem proposition_29' : ∀ (a b c d e g h : Point) (AB CD EF : Line),
-  distinctPointsOnLine a b AB ∧ distinctPointsOnLine c d CD ∧ distinctPointsOnLine g h EF ∧
-  (between a g b) ∧ (between c h d) ∧ (between e g h) ∧ (b.sameSide d EF) ∧ ¬(AB.intersectsLine CD) →
-  ∠ a:g:h = ∠ g:h:d ∧ ∠ e:g:b = ∠ g:h:d ∧ ∠ b:g:h + ∠ g:h:d = ∟ + ∟ :=
-by
-    euclid_intros
-    euclid_apply (extend_point EF g h) as f
-    euclid_apply (proposition_29 a b c d e f g h AB CD EF)
-    euclid_finish
-
-theorem proposition_29'' : ∀ (a b d g h : Point) (AB CD GH : Line),
-  distinctPointsOnLine a b AB ∧ distinctPointsOnLine h d CD ∧ distinctPointsOnLine g h GH ∧
-  (between a g b) ∧ (b.sameSide d GH) ∧ ¬(AB.intersectsLine CD) →
-  ∠ a:g:h = ∠ g:h:d ∧ ∠ b:g:h + ∠ g:h:d = ∟ + ∟ :=
-by
-    euclid_intros
-    euclid_apply (extend_point GH g h) as f
-    euclid_apply (extend_point GH h g) as e
-    euclid_apply (extend_point CD d h) as c
-    euclid_apply (proposition_29 a b c d e f g h AB CD GH)
-    euclid_finish
-
-theorem proposition_29''' : ∀ (a d g h : Point) (AB CD GH : Line),
-  distinctPointsOnLine a g AB ∧ distinctPointsOnLine h d CD ∧ distinctPointsOnLine g h GH ∧
-  a.opposingSides d GH ∧ ¬(AB.intersectsLine CD) →
-  ∠ a:g:h = ∠ g:h:d :=
-by
-  euclid_intros
-  euclid_apply (extend_point AB a g) as b
-  euclid_apply (proposition_29'' a b d g h AB CD GH)
-  euclid_finish
-
-theorem proposition_29'''' : ∀ (b d e g h : Point) (AB CD EF : Line),
-  distinctPointsOnLine g b AB ∧ distinctPointsOnLine h d CD ∧ distinctPointsOnLine e h EF ∧
-  between e g h ∧ b.sameSide d EF ∧ ¬(AB.intersectsLine CD) →
-  ∠ e:g:b = ∠ g:h:d :=
-by
-  euclid_intros
-  euclid_apply (extend_point AB b g) as a
-  euclid_apply (extend_point CD d h) as c
-  euclid_apply (extend_point EF g h) as f
-  euclid_apply (proposition_29 a b c d e f g h AB CD EF)
-  euclid_finish
-
-theorem proposition_29''''' : ∀ (b d g h : Point) (AB CD EF : Line),
-  distinctPointsOnLine g b AB ∧ distinctPointsOnLine h d CD ∧ distinctPointsOnLine g h EF ∧
-  b.sameSide d EF ∧ ¬(AB.intersectsLine CD) →
-  ∠ b:g:h + ∠ g:h:d = ∟ + ∟ :=
-by
-  euclid_intros
-  euclid_apply (extend_point AB b g) as a
-  euclid_apply (extend_point CD d h) as c
-  euclid_apply (extend_point EF g h) as f
-  euclid_apply (extend_point EF h g) as e
-  euclid_apply (proposition_29 a b c d e f g h AB CD EF)
-  euclid_finish
-
-theorem proposition_30 : ∀ (AB CD EF : Line),
-  AB ≠ CD ∧ CD ≠ EF ∧ EF ≠ AB ∧ ¬(AB.intersectsLine EF) ∧ ¬(CD.intersectsLine EF) →
-  ¬(AB.intersectsLine CD) :=
-by
-  euclid_intros
-  euclid_apply (line_nonempty AB) as g
-  euclid_apply (exists_distincts_points_on_line CD g) as k
-  euclid_apply (line_from_points g k) as GK
-  euclid_apply (intersection_lines EF GK) as h
-  euclid_apply (exists_distincts_points_on_line AB g) as a
-  euclid_apply (extend_point AB a g) as b
-  euclid_apply (point_on_line_same_side GK EF a) as e
-  euclid_apply (extend_point EF e h) as f
-  euclid_apply (point_on_line_same_side GK CD a) as c
-  euclid_apply (extend_point CD c k ) as d
-
-  by_cases (between g h k)
-  · euclid_apply (proposition_29'' a b f g h AB EF GK)
-    euclid_apply (proposition_29' e f c d g h k EF CD GK)
-    euclid_apply (proposition_27 a d g k AB CD GK)
-    euclid_finish
-  · -- Omitted by Euclid.
-    by_cases (between g k h)
-    · euclid_apply (proposition_29'' a b f g h AB EF GK)
-      euclid_apply (proposition_29' c d e f g k h CD EF GK)
-      euclid_apply (proposition_27 a d g k AB CD GK)
-      euclid_finish
-    · euclid_apply (proposition_29'' d c e k h CD EF GK)
-      euclid_apply (proposition_29' b a f e k g h AB EF GK)
-      euclid_apply (proposition_27 a d g k AB CD GK)
-      euclid_finish
-
-theorem proposition_31 : ∀ (a b c : Point) (BC : Line),
-  distinctPointsOnLine b c BC ∧ ¬(a.onLine BC) →
-  ∃ EF : Line, a.onLine EF ∧ ¬(EF.intersectsLine BC) :=
-by
-  euclid_intros
-  euclid_apply (exists_point_between_points_on_line BC b c) as d
-  euclid_apply (line_from_points a d) as AD
-  euclid_apply (proposition_23' a d d a c b AD AD BC) as e
-  euclid_apply (line_from_points e a) as EF
-  euclid_apply (extend_point EF e a) as f
-  use EF
-  constructor
-  . euclid_finish
-  . euclid_apply (proposition_27 e c a d EF BC AD)
-    euclid_finish
-
-theorem proposition_32 : ∀ (a b c d : Point) (AB BC AC : Line),
-  formTriangle a b c AB BC AC ∧ (between b c d) →
-  ∠ a:c:d = ∠ c:a:b + ∠ a:b:c ∧
-  ∠ a:b:c + ∠ b:c:a + ∠ c:a:b = ∟ + ∟ :=
-by
-  euclid_intros
-
-  have : (∠ a:c:d : ℝ) = (∠ c:a:b) + (∠ a:b:c) := by
-    euclid_apply (proposition_31 c a b AB ) as CE
-    euclid_apply (point_on_line_same_side BC CE a ) as e
-    euclid_apply (proposition_29''' b e a c AB CE AC)
-    euclid_apply (proposition_29'''' e a d c b CE AB BC)
-    euclid_finish
-
-  constructor
-  · assumption
-  · euclid_apply (proposition_13 a c b d AC BC)
-    euclid_finish
-
-theorem proposition_33 : ∀ (a b c d : Point) (AB CD AC BD : Line),
-  distinctPointsOnLine a b AB ∧ distinctPointsOnLine c d CD ∧
-  distinctPointsOnLine a c AC ∧ distinctPointsOnLine b d BD ∧
-  (a.sameSide c BD) ∧ ¬(AB.intersectsLine CD) ∧ |(a─b)| = |(c─d)| →
-  AC ≠ BD ∧ ¬(AC.intersectsLine BD) ∧ |(a─c)|= |(b─d)| :=
-by
-  euclid_intros
-  euclid_apply (line_from_points b c ) as BC
-  euclid_apply (proposition_29''' a d b c AB CD BC)
-  euclid_apply (proposition_4 c b d b c a BC BD CD BC AC AB)
-  euclid_apply (proposition_27 a d c b AC BD BC)
-  euclid_finish
-
-theorem proposition_34 : ∀ (a b c d : Point) (AB CD AC BD BC : Line),
-  formParallelogram a b c d AB CD AC BD ∧ distinctPointsOnLine b c BC →
-  |(a─b)| = |(c─d)| ∧ |(a─c)| = |(b─d)| ∧
-  ∠ a:b:d = ∠ a:c:d ∧ ∠ b:a:c  = ∠ c:d:b ∧
-  Triangle.area △ a:b:c = Triangle.area △ d:c:b :=
-by
-  euclid_intros
-  euclid_apply (proposition_29''' a d b c AB CD BC)
-  euclid_apply (proposition_29''' a d c b AC BD BC)
-  euclid_apply (proposition_26 a b c d c b AB BC AC CD BC BD)
-  euclid_finish
-
-theorem proposition_34' : ∀ (a b c d : Point) (AB CD AC BD : Line),
-  formParallelogram a b c d AB CD AC BD →
-  |(a─b)| = |(c─d)| ∧ |(a─c)| = |(b─d)| ∧
-  ∠ a:b:d = ∠ a:c:d ∧ ∠ b:a:c = ∠ c:d:b :=
-by
-  euclid_intros
-  euclid_apply (line_from_points b c) as BC
-  euclid_apply (proposition_34 a b c d AB CD AC BD BC)
-  euclid_finish
-
-theorem proposition_35 : ∀ (a b c d e f g : Point) (AF BC AB CD EB FC : Line),
-  formParallelogram a d b c AF BC AB CD ∧ formParallelogram e f b c AF BC EB FC ∧
-  between a d e ∧ between d e f ∧ g.onLine CD ∧ g.onLine EB →
-  Triangle.area △a:b:d + Triangle.area △d:b:c = Triangle.area △e:b:c + Triangle.area △ e:c:f :=
-by
-  euclid_intros
-  euclid_apply (proposition_34' a d b c AF BC AB CD)
-  euclid_apply (proposition_34' e f b c AF BC EB FC)
-  euclid_assert (|(a─d)| = |(e─f)|)
-  euclid_assert (|(a─e)| = |(d─f)|)
-  euclid_apply (proposition_29'''' c b f d a CD AB AF)
-  euclid_apply (proposition_4 a e b d f c AF EB AB AF FC CD)
-  euclid_finish
-
-theorem proposition_35' : ∀ (a b c d e f : Point) (AF BC AB CD EB FC : Line),
-  formParallelogram a d b c AF BC AB CD ∧ formParallelogram e f b c AF BC EB FC →
-  Triangle.area △a:b:d  + Triangle.area △d:b:c = Triangle.area △e:b:c + Triangle.area △ e:c:f :=
-by
-  euclid_intros
-  euclid_apply (proposition_34' a d b c AF BC AB CD)
-  euclid_apply (proposition_34' e f b c AF BC EB FC)
-  euclid_assert (|(a─d)| = |(e─f)|)
-  by_cases (between a d f)
-  · euclid_apply (intersection_lines CD EB) as g
-    by_cases (between a d e)
-    · euclid_apply (proposition_35 a b c d e f g AF BC AB CD EB FC)
-      euclid_finish
-    · euclid_apply (proposition_29'''' c b f d a CD AB AF)
-      euclid_apply (proposition_4 a e b d f c AF EB AB AF FC CD)
-      euclid_finish
-  · by_cases (a = e)
-    · euclid_finish
-    · euclid_apply (intersection_lines FC AB) as g
-      by_cases (between e f a)
-      · euclid_apply (proposition_35 e b c f a d g AF BC EB FC AB CD)
-        euclid_finish
-      · euclid_apply (proposition_29'''' c b d f e FC EB AF)
-        euclid_apply (proposition_4 e a b f d c AF AB EB AF CD FC)
-        by_cases (f = a)
-        · euclid_finish
-        · euclid_assert (Triangle.area △ e:a:b + Triangle.area △ g:b:c = Triangle.area △ f:d:c + Triangle.area △ g:b:c)
-          euclid_finish
-
-theorem proposition_36 : ∀ (a b c d e f g h : Point) (AH BG AB CD EF HG : Line),
-  formParallelogram a d b c AH BG AB CD ∧ formParallelogram e h f g AH BG EF HG ∧
-  |(b─c)| = |(f─g)| ∧ (between a d h) ∧ (between a e h) →
-  Triangle.area △ a:b:d + Triangle.area △ d:b:c = Triangle.area △ e:f:h + Triangle.area △ h:f:g :=
-by
-  euclid_intros
-  euclid_apply (line_from_points b e) as BE
-  euclid_apply (line_from_points c h) as CH
-  euclid_apply (proposition_34' e h f g AH BG EF HG)
-  euclid_assert (|(b─c)| = |(e─h)|)
-  euclid_apply (proposition_33 e h b c AH BG BE CH)
-  euclid_apply (proposition_35' a b c d e h AH BG AB CD BE CH)
-  euclid_apply (proposition_35' g h e f c b BG AH HG EF CH BE)
-  euclid_finish
-
-theorem proposition_36' : ∀ (a b c d e f g h : Point) (AH BG AB CD EF HG : Line) ,
-  formParallelogram a d b c AH BG AB CD ∧ formParallelogram e h f g AH BG EF HG ∧
-  |(b─c)| = |(f─g)| →
-  Triangle.area △ a:b:d + Triangle.area △ d:b:c = Triangle.area △ e:f:h + Triangle.area △ h:f:g :=
-by
-  euclid_intros
-  euclid_apply (line_from_points b e) as BE
-  euclid_apply (line_from_points c h) as CH
-  by_cases (e.sameSide b CH)
-  . euclid_apply (line_from_points h f) as HF
-    euclid_apply (proposition_34 e h f g AH BG EF HG HF)
-    euclid_assert (|(b─c)| = |(e─h)|)
-    euclid_apply (proposition_33 e h b c AH BG BE CH)
-    euclid_assert (formParallelogram e h b c AH BG BE CH)
-    euclid_apply (proposition_35' a b c d e h AH BG AB CD BE CH)
-    euclid_apply (proposition_35' g h e f c b BG AH HG EF CH BE)
-    euclid_finish
-  . euclid_apply (line_from_points b h) as BH
-    euclid_apply (line_from_points c e) as CE
-    euclid_apply (line_from_points e g) as EG
-    euclid_apply (proposition_34 h e g f AH BG HG EF EG)
-    euclid_assert (|(b─c)| = |(e─h)|)
-    euclid_apply (proposition_33 h e b c AH BG BH CE)
-    euclid_assert (formParallelogram h e b c AH BG BH CE)
-    euclid_apply (proposition_35' a b c d h e AH BG AB CD BH CE)
-    euclid_apply (proposition_35' f e h g c b BG AH EF HG CE BH)
-    euclid_finish
-
-theorem proposition_37 : ∀ (a b c d : Point) (AB BC AC BD CD AD : Line),
-  formTriangle a b c AB BC AC ∧ formTriangle d b c BD BC CD ∧ distinctPointsOnLine a d AD ∧
-  ¬(AD.intersectsLine BC) ∧ d.sameSide c AB →
-  Triangle.area △ a:b:c = Triangle.area △ d:b:c :=
-by
-  euclid_intros
-  euclid_apply (proposition_31 b a c AC) as BE
-  euclid_apply (intersection_lines AD BE) as e
-  euclid_apply (proposition_31 c b d BD) as CF
-  euclid_apply (intersection_lines AD CF) as f
-  euclid_apply (proposition_35' e b c a d f AD BC BE AC BD CF)
-  euclid_apply (proposition_34 e a b c AD BC BE AC AB)
-  euclid_apply (proposition_34 f d c b AD BC CF BD CD)
-  euclid_finish
-
-theorem proposition_37' : ∀ (a b c d : Point) (AB BC AC BD CD AD : Line),
-  formTriangle a b c AB BC AC ∧ formTriangle d b c BD BC CD ∧ distinctPointsOnLine a d AD ∧
-  ¬(AD.intersectsLine BC) →
-  Triangle.area △ a:b:c = Triangle.area △ d:b:c :=
-by
-  euclid_intros
-  by_cases (d.sameSide c AB)
-  . euclid_apply (proposition_37 a b c d AB BC AC BD CD AD)
-    assumption
-  . euclid_apply (proposition_37 d b c a BD BC CD AB AC AD)
-    euclid_finish
-
-theorem proposition_38 : ∀ (a b c d e f: Point) (AD BF AB AC DE DF : Line),
-  a.onLine AD ∧ d.onLine AD ∧ formTriangle a b c AB BF AC ∧ formTriangle d e f DE BF DF ∧
-  ¬(AD.intersectsLine BF) ∧ (between b c f) ∧ (between b e f) ∧ |(b─c)| = |(e─f)| →
-  Triangle.area △ a:b:c = Triangle.area △ d:e:f :=
-by
-  euclid_intros
-  euclid_apply (proposition_31 b a c AC) as BG
-  euclid_apply (intersection_lines AD BG) as g
-  euclid_apply (proposition_31 f d e DE) as FH
-  euclid_apply (intersection_lines AD FH) as h
-  euclid_apply (proposition_36' g b c a d e f h AD BF BG AC DE FH)
-  euclid_apply (proposition_34 g a b c AD BF BG AC AB)
-  euclid_apply (proposition_34 e f d h BF AD DE FH DF)
-  euclid_finish
-
-theorem proposition_39 : ∀ (a b c d : Point) (AB BC AC BD CD AD : Line),
-  formTriangle a b c AB BC AC ∧ formTriangle d b c BD BC CD ∧ a.sameSide d BC ∧
-  (△ a:b:c : ℝ) = (△ d:b:c) ∧ distinctPointsOnLine a d AD →
-  ¬(AD.intersectsLine BC) :=
-by
-  euclid_intros
-  by_contra
-  by_cases c.sameSide d AB
-  . euclid_apply (proposition_31 a b c BC) as AE
-    euclid_apply (intersection_lines AE BD) as e
-    euclid_apply (line_from_points e c) as EC
-    euclid_apply (proposition_37 a b c e AB BC AC BD EC AE)
-    euclid_assert (△ e:b:c : ℝ) = (△ d:b:c)
-    euclid_finish
-  . -- Omitted by Euclid.
-    euclid_assert a.sameSide c BD
-    euclid_apply (proposition_31 d b c BC) as DE
-    euclid_apply (intersection_lines DE AB) as e
-    euclid_apply (line_from_points e c) as EC
-    euclid_apply (proposition_37 d b c e BD BC CD AB EC DE)
-    euclid_assert (△ e:b:c : ℝ) = (△ a:b:c)
-
-    -- Not sure why this is necessary.
-    by_cases (between a e b)
-    · euclid_apply (sum_areas_if a b e c AB)
-      euclid_assert e = a
-      euclid_finish
-    · euclid_assert (between e a b)
-      euclid_apply (sum_areas_if e b a c AB)
-      euclid_assert e = a
-      euclid_finish
-
-theorem proposition_40 : ∀  (a b c d e : Point) (AB BC AC CD DE AD : Line),
-  formTriangle a b c AB BC AC ∧ formTriangle d c e CD BC DE ∧ a.sameSide d BC ∧ b ≠ e ∧ |(b─c)| = |(c─e)| ∧
-  distinctPointsOnLine a d AD ∧ (Triangle.area △ a:b:c = Triangle.area △ d:c:e) →
-  ¬(AD.intersectsLine BC) :=
-by
-  euclid_intros
-  by_contra
-  euclid_apply (proposition_31 a b c BC) as AF
-  euclid_apply (intersection_lines AF CD) as f
-  by_cases (a = f)
-  . -- Omitted by Euclid.
-    euclid_apply (intersection_lines AF DE) as g
-    euclid_apply (line_from_points g c) as GC
-    euclid_apply (proposition_38 a b c g c e AF BC AB AC GC DE)
-    euclid_assert (Triangle.area △ d:c:e : ℝ) = (Triangle.area △ g:c:e)
-    euclid_finish
-  . euclid_apply (line_from_points f e) as FE
-    euclid_apply (proposition_38 a b c f c e AF BC AB AC CD FE)
-    euclid_assert ((Triangle.area △ d:c:e : ℝ) = Triangle.area △ f:c:e)
-    euclid_finish
-
-theorem proposition_41 : ∀ (a b c d e : Point) (AE BC AB CD BE CE : Line),
-  formParallelogram a d b c AE BC AB CD ∧ formTriangle e b c BE BC CE ∧ e.onLine AE ∧ ¬(AE.intersectsLine  BC) →
-  (Triangle.area △ a:b:c : ℝ) + (Triangle.area △ a:c:d) = (Triangle.area △ e:b:c) + (Triangle.area △ e :b :c) :=
-by
-  euclid_intros
-  euclid_apply (line_from_points a c) as AC
-  by_cases (a = e)
-  . -- Omitted by Euclid.
-    euclid_assert (Triangle.area △ a:b:c : ℝ) = (Triangle.area △ e:b:c)
-    euclid_apply (proposition_34 d a c b AE BC CD AB AC)
-    euclid_finish
-  . euclid_apply (proposition_37' a b c e AB BC AC BE CE AE)
-    euclid_apply (proposition_34 d a c b AE BC CD AB AC)
-    euclid_finish
-
-theorem proposition_42 : ∀ (a b c d₁ d₂ d₃ : Point) (AB BC AC D₁₂ D₂₃: Line),
-  formTriangle a b c AB BC AC ∧ formRectilinearAngle d₁ d₂ d₃ D₁₂ D₂₃ ∧
-  (∠ d₁:d₂:d₃ : ℝ) > 0 ∧ (∠ d₁:d₂:d₃ : ℝ) < ∟ + ∟ →
-  ∃ (f g e c' : Point) (FG EC EF CG : Line), formParallelogram f g e c' FG EC EF CG ∧
-  (∠ c':e:f = ∠ d₁:d₂:d₃) ∧ (Triangle.area △ f:e:c' + Triangle.area △ f:c':g = Triangle.area △ a:b:c) :=
-by
-  euclid_intros
-  euclid_apply (proposition_10 b c BC) as e
-  euclid_apply (line_from_points a e) as AE
-  euclid_apply (proposition_23' e c d₂ d₁ d₃ a BC D₁₂ D₂₃) as f'
-  euclid_apply (line_from_points e f') as EF
-  euclid_apply (proposition_31 a b c BC) as AG
-  euclid_apply (intersection_lines AG EF) as f
-  euclid_apply (proposition_31 c e f EF) as CG
-  euclid_apply (intersection_lines CG AG) as g
-  euclid_assert (formParallelogram f g e c AG BC EF CG)
-  euclid_apply (proposition_38 a b e a e c AG BC AB AE AE AC)
-  euclid_apply (proposition_41 f e c g a AG BC EF CG AE AC)
-  use f, g, e, c, AG, BC, EF, CG
-  euclid_finish
-
-theorem proposition_42' : ∀ (a b c d₁ d₂ d₃ e : Point) (AB BC AC D₁₂ D₂₃: Line),
-  formTriangle a b c AB BC AC ∧ formRectilinearAngle d₁ d₂ d₃ D₁₂ D₂₃ ∧ between b e c ∧ (|(b─e)| = |(e─c)|) ∧
-  (∠ d₁:d₂:d₃ : ℝ) > 0 ∧ (∠ d₁:d₂:d₃ : ℝ) < ∟ + ∟ →
-  ∃ (f g : Point) (FG EF CG : Line), a.sameSide f BC ∧ formParallelogram f g e c FG BC EF CG ∧
-  (∠ c:e:f : ℝ) = (∠ d₁:d₂:d₃) ∧ (Triangle.area △ f:e:c : ℝ) + (Triangle.area △ f:c:g) = (Triangle.area △ a:b:c) :=
-by
-  euclid_intros
-  euclid_apply (line_from_points a e) as AE
-  euclid_apply (proposition_23' e c d₂ d₁ d₃ a BC D₁₂ D₂₃) as fn
-  euclid_apply (line_from_points e fn) as EF
-  euclid_apply (proposition_31 a b c BC) as AG
-  euclid_apply (intersection_lines AG EF) as f
-  euclid_apply (proposition_31 c e f EF) as CG
-  euclid_apply (intersection_lines CG AG) as g
-  euclid_assert (formParallelogram f g e c AG BC EF CG)
-  euclid_apply (proposition_38 a b e a e c AG BC AB AE AE AC)
-  euclid_apply (proposition_41 f e c g a AG BC EF CG AE AC)
-  use f, g, AG, EF, CG
-  euclid_finish
-
-theorem proposition_42'' : ∀ (a b c d₁ d₂ d₃ h i : Point) (AB BC AC D₁₂ D₂₃ HI : Line),
-  formTriangle a b c AB BC AC ∧ formRectilinearAngle d₁ d₂ d₃ D₁₂ D₂₃ ∧
-  (∠ d₁:d₂:d₃ : ℝ) > 0 ∧ (∠ d₁:d₂:d₃ : ℝ) < ∟ + ∟ ∧ distinctPointsOnLine h i HI →
-  ∃ (f g j : Point) (FG FI GJ : Line), between h i j ∧ formParallelogram f g i j FG HI FI GJ ∧
-  (∠ j:i:f : ℝ) = (∠ d₁:d₂:d₃) ∧ (Triangle.area △ f:i:j : ℝ) + (Triangle.area △ f:j:g) = (Triangle.area △ a:b:c) :=
-by
-  euclid_intros
-  euclid_apply (proposition_10 b c BC) as e
-  euclid_apply (extend_point_longer HI h i (e─c)) as i''
-  euclid_apply (proposition_3 i i'' e c HI BC) as j
-  euclid_apply (extend_point_longer HI i h (e─c)) as h'
-  euclid_apply (proposition_3 i h' e c HI BC) as k
-  euclid_apply (proposition_23 k j b a c HI AB BC) as l'
-  euclid_apply (line_from_points k l') as KL
-  euclid_apply (extend_point_longer KL k l' (a─b)) as l''
-  euclid_apply (proposition_3 k l'' b a KL AB) as l
-  euclid_apply (line_from_points l j) as LJ
-  euclid_apply (proposition_4 k j l b c a HI LJ KL BC AC AB)
-  euclid_apply (proposition_42' l k j d₁ d₂ d₃ i KL HI LJ D₁₂ D₂₃) as (f, g, FG, FI, GJ)
-  use f, g, j, FG, FI, GJ
-  euclid_finish
-
-theorem proposition_42''' : ∀ (a b c d₁ d₂ d₃ h i x : Point) (AB BC AC D₁₂ D₂₃ HI : Line),
-  formTriangle a b c AB BC AC ∧ formRectilinearAngle d₁ d₂ d₃ D₁₂ D₂₃ ∧ ¬(x.onLine HI) ∧
-  (∠ d₁:d₂:d₃ : ℝ) > 0 ∧ (∠ d₁:d₂:d₃ : ℝ) < ∟ + ∟ ∧ distinctPointsOnLine h i HI →
-  ∃ (f g j : Point) (FG FI GJ : Line), f.sameSide x HI ∧ between h i j ∧ formParallelogram f g i j FG HI FI GJ ∧
-  (∠ j:i:f : ℝ) = (∠ d₁:d₂:d₃) ∧ (Triangle.area △ f:i:j : ℝ) + (Triangle.area △ f:j:g) = (Triangle.area △ a:b:c) :=
-by
-  euclid_intros
-  euclid_apply (proposition_10 b c BC) as e
-  euclid_apply (extend_point_longer HI h i (e─c)) as i''
-  euclid_apply (proposition_3 i i'' e c HI BC) as j
-  euclid_apply (extend_point_longer HI i h (e─c)) as h'
-  euclid_apply (proposition_3 i h' e c HI BC) as k
-  euclid_apply (proposition_23' k j b a c x HI AB BC) as l'
-  euclid_apply (line_from_points k l') as KL
-  euclid_apply (extend_point_longer KL k l' (a─b)) as l''
-  euclid_apply (proposition_3 k l'' b a KL AB) as l
-  euclid_apply (line_from_points l j) as LJ
-  euclid_apply (proposition_4 k j l b c a HI LJ KL BC AC AB)
-  euclid_apply (proposition_42' l k j d₁ d₂ d₃ i KL HI LJ D₁₂ D₂₃) as (f, g, FG, FI, GJ)
-  use f, g, j, FG, FI, GJ
-  euclid_finish
-
-theorem proposition_43 : ∀ (a b c d e f g h k : Point) (AD BC AB CD AC EF GH : Line),
-  formParallelogram a d b c AD BC AB CD ∧ distinctPointsOnLine a c AC ∧ k.onLine AC ∧
-  between a h d ∧ formParallelogram a h e k AD EF AB GH ∧ formParallelogram k f g c EF BC GH CD →
-  (Triangle.area △ e:b:g + Triangle.area △ e:g:k = Triangle.area △ h:k:f + Triangle.area △ h:f:d) :=
-by
-  euclid_intros
-  euclid_apply (proposition_34 d a c b AD BC CD AB AC)
-  euclid_apply (proposition_34 h a k e AD EF GH AB AC)
-  euclid_apply (proposition_34 f k c g EF BC CD GH AC)
-  euclid_assert (Triangle.area △ a:e:k : ℝ) + (Triangle.area △ k:g:c) = (Triangle.area △ a:h:k) + (Triangle.area △ k:f:c)
-  euclid_assert (Triangle.area △ a:h:k : ℝ) + (Triangle.area △ k:f:c) + (Triangle.area △ h:k:f) + (Triangle.area △ h:f:d) = (Triangle.area △ d:a:c)
-  euclid_finish
-
-theorem proposition_44 : ∀ (a b c₁ c₂ c₃ d₁ d₂ d₃ : Point) (AB C₁₂ C₂₃ C₃₁ D₁₂ D₂₃ : Line),
-  formTriangle c₁ c₂ c₃ C₁₂ C₂₃ C₃₁ ∧ formRectilinearAngle d₁ d₂ d₃ D₁₂ D₂₃ ∧ distinctPointsOnLine a b AB ∧
-  (∠ d₁:d₂:d₃ : ℝ) > 0 ∧ (∠ d₁:d₂:d₃ : ℝ) < ∟ + ∟ →
-  ∃ (m l : Point) (BM AL ML : Line), formParallelogram b m a l BM AL AB ML ∧
-  (∠ a:b:m = ∠ d₁:d₂:d₃) ∧ (Triangle.area △ a:b:m + Triangle.area △ a:l:m = Triangle.area △ c₁:c₂:c₃) :=
-by
-  euclid_intros
-  euclid_apply (proposition_42'' c₁ c₂ c₃ d₁ d₂ d₃ a b C₁₂ C₂₃ C₃₁ D₁₂ D₂₃ AB) as (g, f, e, FG, BG, EF)
-  euclid_apply (proposition_31 a b g BG) as AH
-  euclid_apply (proposition_30 AH EF BG)
-  euclid_apply (intersection_lines AH FG) as h
-  euclid_apply (line_from_points h b) as HB
-  euclid_apply (proposition_29''''' e a f h EF AH FG)
-  euclid_apply (intersection_lines HB EF) as k
-  euclid_apply (proposition_31 k e a AB) as KL
-  euclid_apply (proposition_30 KL FG AB)
-  euclid_apply (intersection_lines AH KL) as l
-  euclid_apply (intersection_lines BG KL) as m
-  euclid_apply (proposition_43 h f k l g m e a b AH EF FG KL HB BG AB)
-  euclid_apply (proposition_15 e a m g b AB BG)
-  use m, l, BG, AH, KL
-  euclid_finish
-
-theorem proposition_44' : ∀ (a b c₁ c₂ c₃ d₁ d₂ d₃ x : Point) (AB C₁₂ C₂₃ C₃₁ D₁₂ D₂₃ : Line),
-  formTriangle c₁ c₂ c₃ C₁₂ C₂₃ C₃₁ ∧ formRectilinearAngle d₁ d₂ d₃ D₁₂ D₂₃ ∧ distinctPointsOnLine a b AB ∧ ¬(x.onLine AB) ∧
-  (∠ d₁:d₂:d₃ : ℝ) > 0 ∧ (∠ d₁:d₂:d₃ : ℝ) < ∟ + ∟ →
-  ∃ (m l : Point) (BM AL ML : Line), Point.opposingSides m x AB ∧ formParallelogram b m a l BM AL AB ML ∧
-  (∠ a:b:m : ℝ) = (∠ d₁:d₂:d₃) ∧ (Triangle.area △ a:b:m) + (Triangle.area △ a:l:m) = (Triangle.area △ c₁:c₂:c₃) :=
-by
-  euclid_intros
-  euclid_apply (proposition_42''' c₁ c₂ c₃ d₁ d₂ d₃ a b x C₁₂ C₂₃ C₃₁ D₁₂ D₂₃ AB) as (g, f ,e ,FG, BG, EF)
-  euclid_apply (proposition_31 a b g BG) as AH
-  euclid_apply (proposition_30 AH EF BG)
-  euclid_apply (intersection_lines AH FG) as h
-  euclid_apply (line_from_points h b) as HB
-  euclid_apply (proposition_29''''' e a f h EF AH FG)
-  euclid_apply (intersection_lines HB EF) as k
-  euclid_apply (proposition_31 k e a AB) as KL
-  euclid_apply (proposition_30 KL FG AB)
-  euclid_apply (intersection_lines AH KL) as l
-  euclid_apply (intersection_lines BG KL) as m
-  euclid_apply (proposition_43 h f k l g m e a b AH EF FG KL HB BG AB)
-  euclid_apply (proposition_15 e a m g b AB BG)
-  use m, l, BG, AH, KL
-  euclid_finish
-
-theorem proposition_45 : ∀ (a b c d e₁ e₂ e₃ : Point) (AB BC CD AD DB E₁₂ E₂₃ : Line),
-  formTriangle a b d AB DB AD ∧ formTriangle b c d BC CD DB ∧ a.opposingSides c DB ∧
-  formRectilinearAngle e₁ e₂ e₃ E₁₂ E₂₃ ∧ ∠ e₁:e₂:e₃ > 0 ∧ ∠ e₁:e₂:e₃ < ∟ + ∟ →
-  ∃ (f l k m : Point) (FL KM FK LM : Line), formParallelogram f l k m FL KM FK LM ∧
-  (∠ f:k:m = ∠ e₁:e₂:e₃) ∧ (Triangle.area △ f:k:m + Triangle.area △ f:l:m = Triangle.area △ a:b:d + Triangle.area △ d:b:c) :=
-by
-  euclid_intros
-  euclid_apply (proposition_42 a b d e₁ e₂ e₃ AB DB AD E₁₂ E₂₃) as (f, g, k, h , FG, KH, FK, GH)
-  euclid_apply (proposition_44' g h d b c e₁ e₂ e₃ k GH DB BC CD E₁₂ E₂₃) as (m, l, HM, G, LM)
-  euclid_assert ((∠ h:k:f : ℝ) = ∠ g:h:m)
-  euclid_assert ((∠ h:k:f : ℝ) + (∠ k:h:g) = (∠ g:h:m) + (∠ k:h:g))
-  euclid_apply (proposition_29''''' f g k h FK GH KH)
-  euclid_assert ((∠ k:h:g : ℝ) + (∠ g:h:m) = ∟ + ∟)
-  euclid_apply (proposition_14 g h k m GH KH HM)
-  euclid_apply (proposition_29''' f m g h FG HM GH)
-  euclid_assert ((∠ m:h:g : ℝ) + (∠ h:g:l) = (∠ h:g:f) + (∠ h:g:l))
-  euclid_apply (proposition_29''''' l m g h G HM GH)
-  euclid_assert ((∠ h:g:f : ℝ) + (∠ h:g:l) = ∟ + ∟)
-  euclid_apply (proposition_14 h g f l GH FG G)
-  euclid_apply (proposition_34' f g k h FG KH FK GH)
-  euclid_apply (proposition_34' h m g l HM G GH LM)
-  euclid_assert (|(k─f)| = |(m─l)|)
-  euclid_apply (proposition_30 FK LM GH)
-  euclid_assert (|(f─l)| = |(k─m)|)
-  euclid_apply (proposition_33 f l k m FG KH FK LM)
-  use f, l, k, m, FG, KH, FK, LM
-  euclid_finish
-
-theorem proposition_46 : ∀ (a b : Point) (AB : Line), distinctPointsOnLine a b AB →
-  ∃ (d e : Point) (DE AD BE : Line), formParallelogram d e a b DE AB AD BE ∧
-  |(d─e)| = |(a─b)| ∧ |(a─d)| = |(a─b)| ∧ |(b─e)| = |(a─b)| ∧
-  (∠ b:a:d = ∟) ∧ (∠ a:d:e = ∟) ∧ (∠ a:b:e = ∟) ∧ (∠ b:e:d = ∟) :=
-by
-  euclid_intros
-  euclid_apply (proposition_11'' a b AB) as c'
-  euclid_apply (line_from_points a c') as AC
-  euclid_apply (extend_point_longer AC a c' (a─b)) as c
-  euclid_apply (proposition_3 a c a b AC AB) as d
-  euclid_apply (proposition_31 d a b AB) as DE
-  euclid_apply (proposition_31 b a d AC) as BE
-  euclid_apply (intersection_lines DE BE) as e
-  euclid_apply (proposition_34' d e a b DE AB AC BE)
-  euclid_apply (proposition_29''''' e b d a DE AB AC)
-  euclid_apply (proposition_34' d e a b DE AB AC BE)
-  use d, e, DE, AC, BE
-  euclid_finish
-
-theorem proposition_46' : ∀ (a b x : Point) (AB : Line), ¬(x.onLine AB) ∧ distinctPointsOnLine a b AB →
-  ∃ (d e : Point) (DE AD BE : Line), d.opposingSides x AB ∧ formParallelogram d e a b DE AB AD BE ∧
-  |(d─e)| = |(a─b)| ∧ |(a─d)| = |(a─b)| ∧ |(b─e)| = |(a─b)| ∧
-  (∠ b:a:d : ℝ) = ∟ ∧ (∠ a:d:e : ℝ) = ∟ ∧ (∠ a:b:e : ℝ) = ∟ ∧ (∠ b:e:d : ℝ) = ∟ :=
-by
-  euclid_intros
-  euclid_apply (proposition_11''' a b x AB) as c'
-  euclid_apply (line_from_points a c') as AC
-  euclid_apply (extend_point_longer AC a c' (a─b)) as c
-  euclid_apply (proposition_3 a c a b AC AB) as d
-  euclid_apply (proposition_31 d a b AB) as DE
-  euclid_apply (proposition_31 b a d AC) as BE
-  euclid_apply (intersection_lines DE BE) as e
-  euclid_apply (proposition_34' d e a b DE AB AC BE)
-  euclid_apply (proposition_29''''' e b d a DE AB AC)
-  euclid_apply (proposition_34' d e a b DE AB AC BE)
-  use d, e, DE, AC, BE
-  euclid_finish
-
--- WARNING: This proof is quite slow.
-set_option maxHeartbeats 0 in
-theorem proposition_47 : ∀ (a b c: Point) (AB BC AC : Line),
-  formTriangle a b c AB BC AC ∧ (∠ b:a:c : ℝ) = ∟ →
-  |(b─c)| * |(b─c)| = |(b─a)| * |(b─a)| + |(a─c)| * |(a─c)| :=
-by
-  euclid_intros
-  euclid_apply (proposition_46' b a c AB) as (f, g, FG, BF, AG)
-  euclid_apply (proposition_46' a c b AC) as (h, k, HK, AH, CK)
-  euclid_apply (proposition_46' b c a BC) as (d, e, DE, BD, CE)
-
-  -- Missed by Euclid.
-  have : (∠ a:b:c : ℝ) < ∟ := by
-    euclid_apply (proposition_17 c a b AC AB BC)
-    euclid_finish
-
-  -- Missed by Euclid.
-  have : ¬(d.onLine AB) := by
-    by_contra
-    euclid_apply (proposition_13 c b a d BC AB)
-    euclid_finish
-
-  -- Missed by Euclid.
-  have : (d.sameSide c AB) := by
-    euclid_apply (extend_point AB a b) as b'
-    euclid_apply (proposition_16 c a b b' AC AB BC)
-    euclid_assert (∠ c:b:b' : ℝ) > ∟
-    euclid_finish
-
-  -- Missed by Euclid.
-  have : (∠ a:c:b : ℝ) < ∟ := by
-    euclid_apply (proposition_17 b c a BC AC AB)
-    euclid_finish
-
-  -- Missed by Euclid.
-  have : ¬(e.onLine AC) := by
-    by_contra
-    euclid_apply (proposition_13 b c a e BC AC)
-    euclid_finish
-
-  -- Missed by Euclid.
-  have : (e.sameSide b AC) := by
-    euclid_apply (extend_point AC a c) as c'
-    euclid_apply (proposition_16 b a c c' AB AC BC)
-    euclid_assert (∠ b:c:c' : ℝ) > ∟
-    euclid_finish
-
-  euclid_apply (proposition_31 a b d BD) as AL
-  euclid_apply (proposition_30 AL CE BD)
-  euclid_apply (intersection_lines AL DE) as l
-  euclid_apply (intersection_lines AL BC) as l'
-  euclid_apply (line_from_points a d) as AD
-  euclid_apply (line_from_points f c) as FC
-  euclid_apply (proposition_14 b a c g AB AC AG)
-  euclid_apply (proposition_14 c a b h AC AB AH)
-  euclid_assert ((∠ d:b:a : ℝ) = ∠ f:b:c)
-  euclid_assert ((∠ c:b:a : ℝ) + ∟ = ∠ c:b:f)
-  euclid_apply (proposition_4 b d a b c f BD AD AB BC FC BF)
-  euclid_assert ((Triangle.area △ a:b:d) = Triangle.area △ b:c:f)
-  euclid_apply (proposition_41 l' b d l a AL BD BC DE AB AD)
-  euclid_apply (proposition_41 g f b a c AG BF FG AB FC BC)
-  euclid_assert ((Triangle.area △ g:f:b : ℝ) + (Triangle.area △ g:b:a) = (Triangle.area △ l':b:d) + (Triangle.area △ l':d:l))
-  euclid_apply (line_from_points a e) as AE
-  euclid_apply (line_from_points b k) as BK
-  euclid_apply sum_angles_onlyif c e a b CE AC
-  euclid_apply sum_angles_onlyif c k b a CK BC
-  euclid_assert ((∠ e:c:a : ℝ) = (∠ k:c:b))
-  euclid_apply (proposition_4 c e a c b k CE AE AC BC BK CK)
-  euclid_assert ((Triangle.area △ a:c:e : ℝ) = Triangle.area △ c:b:k)
-  euclid_apply (proposition_41 l' c e l a AL CE BC DE AC AE)
-  euclid_apply (proposition_41 h k c a b AH CK HK AC BK BC)
-  euclid_assert ((Triangle.area △ k:c:a : ℝ) + (Triangle.area △ k:a:h) = (Triangle.area △ l':c:e) + (Triangle.area △ l':e:l))
-  euclid_apply (rectangle_area b c d e BC DE BD CE)
-  euclid_apply (rectangle_area b a f g AB FG BF AG)
-  euclid_apply (rectangle_area a c h k AC HK AH CK)
-  euclid_apply sum_parallelograms_area b c d e l' l BC DE BD CE
-  euclid_apply parallelogram_area b l' d l BC DE BD AL
-  euclid_assert ((Triangle.area △ b:d:e : ℝ) + (Triangle.area △ b:e:c) = (Triangle.area △ g:f:b) + (Triangle.area △ g:b:a) + (Triangle.area △ k:c:a) + (Triangle.area △ k:a:h))
-  euclid_finish
-
-theorem proposition_48 : ∀ (a b c : Point) (AB BC AC : Line),
-  formTriangle a b c AB BC AC ∧ |(b─c)| * |(b─c)| = |(b─a)| * |(b─a)| + |(a─c)| * |(a─c)| →
-  ∠ b:a:c = ∟ :=
-by
-  euclid_intros
-  euclid_apply (proposition_11'' a c AC) as d'
-  euclid_apply (line_from_points a d') as AD
-  euclid_apply (extend_point AD d' a) as d''
-  euclid_apply (extend_point_longer AD d'' a (a─b)) as d'''
-  euclid_apply (proposition_3 a d''' a b AD AB) as d
-  euclid_apply (line_from_points d c) as DC
-  euclid_assert (|(d─a)| * |(d─a)| = |(a─b)| * |(a─b)|)
-  euclid_assert (|(d─a)| * |(d─a)| + |(a─c)| * |(a─c)| = |(a─b)| * |(a─b)| + |(a─c)| * |(a─c)|)
-  euclid_apply (proposition_47 a d c AD DC AC)
-  euclid_assert (|(d─c)| = |(b─c)|)
-  euclid_apply (proposition_8 a b c a d c AB BC AC AD DC AC)
-  euclid_finish
-
-
-end Elements