proposition: Lemma l12_22 : 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. split; intro. apply (l12_22_b _ _ _ _ P); assumption. apply l12_22_a; assumption. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID