proposition: Lemma l6_11_existence : forall A B C R, R<>A -> B<>C -> exists X, Out A X R /\ Cong A X B C.
proof: Proof. intros. assert (exists X : Tpoint, (Bet A R X \/ Bet A X R) /\ Cong A X B C) by (apply (segment_construction_2);assumption). ex_and H1 X. exists X. unfold Out;repeat split; try intro;treat_equalities;intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le