proposition: Lemma segment_construction : forall A B C D, exists E, Bet A B E /\ Cong B E C D.
proof: Proof. intros. unfold Bet, Cong. elim (point_eq_dec C D). intros. exists B. tauto. intros. elim (point_eq_dec A B). intro;subst. destruct B; try (exists P0; split; try tauto; right; split; try discriminate; assumption); exists P1; split; try tauto; right; split; try discriminate; assumption. intros; exists A; firstorder. Qed.
imports: GeoCoq.Axioms.tarski_axioms