proposition: Lemma ex_point_lg_out : forall l A P, A <> P -> Q_Cong l -> ~ Q_Cong_Null l -> exists B, l A B /\ Out A B P.
proof: Proof. intros. assert(HH:= H0). unfold Q_Cong in HH. ex_and HH X. ex_and H2 Y. assert(HP:= H3 X Y). destruct HP. assert(l X Y). apply H2. apply cong_reflexivity. assert(X <> Y). intro. subst Y. apply H1. unfold Q_Cong_Null. split. auto. exists X. auto. assert(HH:= segment_construction_3 A P X Y H H6). ex_and HH B. exists B. split. assert(HH:= H3 A B). destruct HH. apply H9. Cong. apply l6_6. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1