proposition: Lemma segment_construction_3 : forall A B X Y, A <> B -> X <> Y -> exists C, Out A B C /\ Cong A C X Y.
proof: Proof. intros. destruct (l6_11_existence A X Y B) as [C [HC1 HC2]]; auto. apply l6_6 in HC1. exists C; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le