proposition: Lemma axiom_euclid_uniqueness : forall l P m1 m2, ~ IncidentL P l -> Para l m1 -> IncidentL P m1 -> Para l m2 -> IncidentL P m2 -> EqL m1 m2.
proof: Proof. intros. destruct l as [A B HAB]. destruct m1 as [C D HCD]. destruct m2 as [C' D' HCD']. unfold IncidentL in *;simpl in *. apply Para_Par in H0. apply Para_Par in H2. elim (tarski_s_euclid_implies_playfair euclid A B C D C' D' P H0 H1 H2 H3);intros. apply axiom_line_uniqueness with C' D'; 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