proposition: Lemma segment_construction : forall A B C D : ITpoint, exists E : ITpoint, BetT A B E /\ ICong B E C D.
proof: Proof. intros. induction (eq_dec A B). subst. elim (another_point B);intros. elim (Isegment_construction x B C D);intros. exists x0. split. unfold BetT. intuition. intuition. intuition. elim (Isegment_construction A B C D H). intros. exists x. spliter. split;try assumption. unfold IT in *. unfold BetT. tauto. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Axioms.tarski_axioms Classical