is_midpoint

is_midpoint := fun M A B => Bet A M B /\ Cong A M M B

l7_2 (symmetry)

forall M A B, is_midpoint M A B → is_midpoint M B A

l7_3 (trivial case)

forall M A, is_midpoint M A A → M = A

l7_3_2 (trivial case)

forall A, is_midpoint A A A

symmetric_point_construction

forall A P, exists A', is_midpoint P A A'

symmetric_point_unicity

forall A P P1 P2, is_midpoint P A P1 → is_midpoint P A P2 → P1 = P2

l7_9 (symmetric point unicity)

forall P Q A B, is_midpoint A P B → is_midpoint A Q B → P=Q

l7_13 (symmetry preserves congruence)

forall A P Q P' Q', is_midpoint A P' P → is_midpoint A Q' Q → Cong P Q P' Q'

l7_15 (symmetry preserves betweeness)

forall P Q R P' Q' R' A, is_midpoint A P P' → is_midpoint A Q Q' → is_midpoint A R R' → Bet P Q R → Bet P' Q' R'

l7_16 (symmetry preserves congruence)

forall P Q R S P' Q' R' S' A,
      is_midpoint A P P' → is_midpoint A Q Q' → is_midpoint A R R' → is_midpoint A S S' → Cong P Q R S → Cong P' Q' R' S'

symmetry_preserves_midpoint

forall A B C D E F Z, is_midpoint Z A D → is_midpoint Z B E → is_midpoint Z C F → is_midpoint B A C → is_midpoint E D F

l7_17 : mid_point unicity

forall P P' A B, is_midpoint A P P' → is_midpoint B P P' → A = B

l7_20

forall M A B, Col A M B → Cong M A M B → A = B \/ is_midpoint M A B

l7_21

forall A B C D P, ~ Col A B C → B <> D → Cong A B C D → Cong B C D A → Col A P C → Col B P D → is_midpoint P A C /\ is_midpoint P B D

l7_22_aux

forall A1 A2 B1 B2 C M1 M2,
      Bet A1 C A2 → Bet B1 C B2 → Cong C A1 C B1 → Cong C A2 C B2 →
      is_midpoint M1 A1 B1 → is_midpoint M2 A2 B2 → le C A1 C A2 → Bet M1 C M2

l7_22

forall A1 A2 B1 B2 C M1 M2,
      Bet A1 C A2 → Bet B1 C B2 → Cong C A1 C B1 → Cong C A2 C B2 →
      is_midpoint M1 A1 B1 → is_midpoint M2 A2 B2 → Bet M1 C M2

l7_25

forall A B C, Cong C A C B → exists X, is_midpoint X A B