proposition: Lemma l12_22_b : forall A B C D P, Out P A C -> OS P A B D -> CongA B A P D C P -> Par A B C D.
proof: Proof. intros. induction(eq_dec_points A C). subst C. unfold Par. right. repeat split. unfold CongA in H1. spliter. auto. unfold CongA in H1. spliter. auto. Col. apply conga_comm in H1. apply conga_os__out in H1; Col. unfold Out in H. spliter. induction H4. apply l12_22_aux with P; auto. apply par_symmetry. apply l12_22_aux with P; auto. apply (col_one_side _ A). apply bet_col in H4. Col. auto. apply one_side_symmetry. assumption. apply conga_sym. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles