proposition: Lemma par_not_par : forall A B C D P Q, Par A B C D -> ~Par A B P Q -> ~Par C D P Q.
proof: Proof. intros A B C D P Q HPar HNPar. intro HNPar'. apply HNPar. apply par_trans with C D; Par. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID