proposition: Lemma axiom_line_uniqueness : forall A B l m, A <> B -> IncidentL A l -> IncidentL B l -> IncidentL A m -> IncidentL B m -> l =l= m.
proof: Proof. intros. assert ((Lin A B H) =l= l). eapply incident_eq;assumption. assert ((Lin A B H) =l= m). eapply incident_eq;assumption. rewrite <- H4. assumption. 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