proposition: Lemma five_segment_B : forall A A' B B' C C' D D' : Tpoint, Cong A B A' B' -> Cong B C B' C' -> Cong A D A' D' -> Cong B D B' D' -> ~ (A <> B /\ B <> C /\ ~ BetH A B C) -> ~ (A' <> B' /\ B' <> C' /\ ~ BetH A' B' C') -> A <> B -> Cong C D C' D'.
proof: Proof. intros. assert (HBet1 : T A B C) by (unfold T; assumption). assert (HBet2 : T A' B' C') by (unfold T; assumption). apply T_Bet in H3. apply T_Bet in H4. apply five_segment with A A' B B'; assumption. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality