Library GeoCoq.Elements.OriginalProofs.euclidean_defs

Require Export GeoCoq.Axioms.euclidean_axioms.

Section Definitions.

Context `{Ax:euclidean_neutral}.

Definition Out A B C := X, BetS X A C BetS X A B.
Definition Lt A B C D := X, BetS C X D Cong C X A B.
Definition Midpoint A B C := BetS A B C Cong A B B C.
Definition CongA A B C a b c := U V u v, Out B A U Out B C V Out b a u Out b c v Cong B U b u Cong B V b v Cong U V u v nCol A B C.
Definition AdjacentAngle A B C D E F := eq B E BetS A B F Out B D C.
Definition VA A B C D E F := eq B E BetS A B D BetS C B F.
Definition Supp A B C D F := Out B C D BetS A B F.
Definition Per A B C := X, BetS A B X Cong A B X B Cong A C X C neq B C.
Definition Perp_at P Q A B C := X, Col P Q C Col A B C Col A B X Per X C P.
Definition Perp P Q A B := X, Perp_at P Q A B X.
Definition InAngle A B C P := X Y, Out B A X Out B C Y BetS X P Y.
Definition OS P Q A B := X U V, Col A B U Col A B V BetS P U X BetS Q V X nCol A B P nCol A B Q.
Definition IO A B C D := BetS A B C BetS A B D BetS A C D BetS B C D.
Definition isosceles A B C := Triangle A B C Cong A B A C.
Definition Cut A B C D E := BetS A E B BetS C E D nCol A B C nCol A B D.
Definition LtA A B C D E F := U X V, BetS U X V Out E D U Out E F V CongA A B C D E X.
Definition TG A B C D E F := X, BetS A B X Cong B X C D Lt E F A X.
Definition TT A B C D E F G H := X, BetS E F X Cong F X G H TG A B C D E X.
Definition RT A B C D E F := X Y Z U V, Supp X Y U V Z CongA A B C X Y U CongA D E F V Y Z.
Definition Meet A B C D := X, neq A B neq C D Col A B X Col C D X.
Definition CR A B C D := X, BetS A X B BetS C X D.
Definition TP A B C D := neq A B neq C D ¬ Meet A B C D OS C D A B.
Definition Par A B C D := U V u v X, neq A B neq C D Col A B U Col A B V neq U V Col C D u Col C D v neq u v ¬ Meet A B C D BetS U X v BetS u X V.
Definition SumA A B C D E F P Q R := X, CongA A B C P Q X CongA D E F X Q R BetS P X R.
Definition PG A B C D := Par A B C D Par A D B C.
Definition SQ A B C D := Cong A B C D Cong A B B C Cong A B D A Per D A B Per A B C Per B C D Per C D A.
Definition RE A B C D := Per D A B Per A B C Per B C D Per C D A CR A C B D.
Definition RC A B C D a b c d := RE A B C D RE a b c d Cong A B a b Cong B C b c.
Definition ER A B C D a b c d := X Y Z U x z u w W, RC A B C D X Y Z U RC a b c d x Y z u BetS x Y Z BetS X Y z BetS W U w.
Definition equilateral A B C := Cong A B B C Cong B C C A.

End Definitions.