proposition: Lemma Para_Par : forall A B C D (HAB : A<>B) (HCD: C<>D), Para (Lin A B HAB) (Lin C D HCD) -> Par A B C D.
proof: Proof. unfold Para, IncidentL, Par, Par_strict; simpl. intros. destruct H as [HNI [p []]]. left. repeat split;auto. apply plane_cop with p; [apply H|apply H|apply H0..]; unfold IncidentL; simpl; Col. Qed.
imports: Morphisms GeoCoq.Axioms.hilbert_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair GeoCoq.Meta_theory.Parallel_postulates.SPP_ID GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Utils.triples