proposition: Lemma par_dec : forall A B C D, Par A B C D \/ ~ Par A B C D.
proof: Proof. exact (par_trans__par_dec par_trans). Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID