proposition: Lemma five_segment' : forall A A' B B' C C' D D', Cong A B A' B' -> Cong B C B' C' -> Cong A D A' D' -> Cong B D B' D' -> Bet A B C -> Bet A' B' C' -> A <> B -> Cong D C C' D'.
proof: Proof. intros. assert(Cong C D C' D'). intros. eapply five_segment with A A' B B';assumption. assert(Cong C D D C). eapply cong_pseudo_reflexivity;eauto. apply cong_inner_transitivity with C D;assumption. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.makarios_variant_axioms