proposition: Lemma ex_points_lg : forall l, Q_Cong l -> exists A, exists B, l A B.
proof: Proof. intros. unfold Q_Cong in H. ex_and H A. ex_and H0 B. assert(HH:= H A B). destruct HH. exists A. exists B. apply H0. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1