From f0fb36e31c4bd33dd4f8035ddb9ce85e8af5d42f Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Sat, 20 Jul 2024 13:09:51 +0200
Subject: [PATCH] added lengths and rightangle proof requirement for cylinder
 scroll

---
 source/Scrolls/CylinderScroll.mmt | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/source/Scrolls/CylinderScroll.mmt b/source/Scrolls/CylinderScroll.mmt
index e78d12a..3e3ff25 100644
--- a/source/Scrolls/CylinderScroll.mmt
+++ b/source/Scrolls/CylinderScroll.mmt
@@ -20,6 +20,21 @@ theory CylinderScroll =
          ❘ meta ?MetaAnnotations?description "The point directly above the point M"
         ❙
 
+        dME: Σ x:ℝ . ⊦ (d- M E) ≐ x
+         ❘ meta ?MetaAnnotations?label "dME"
+         ❘ meta ?MetaAnnotations?description "The distance from point M to point E, effectively being the Radius."
+        ❙
+
+        dMT: Σ x:ℝ . ⊦ (d- M T) ≐ x
+         ❘ meta ?MetaAnnotations?label "dBC"
+         ❘ meta ?MetaAnnotations?description "The distance from point M to point T, the height of the cylinder."
+        ❙
+
+        rEMT: ⊦ (∠ E,M,T) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label "rEMT"
+         ❘ meta ?MetaAnnotations?description "A right angle between E, M and T, starting at E."
+        ❙
+
 
         
     ❚
-- 
GitLab