proposition: Lemma five_segment: forall A A' B B' C C' D D' : ITpoint, ICong A B A' B' -> ICong B C B' C' -> ICong A D A' D' -> ICong B D B' D' -> BetT A B C -> BetT A' B' C' -> A <> B -> ICong C D C' D'.
proof: Proof. intros. apply Ifive_segment with A A' B B' ;try assumption. unfold IT. intro. spliter. unfold BetT in *. intuition. unfold BetT in *. unfold IT. intro. intuition. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Axioms.tarski_axioms Classical