proposition: Lemma incident_eq : forall A B l, forall H : A<>B, IncidentL A l -> IncidentL B l -> (Lin A B H) =l= l.
proof: Proof. intros. unfold EqL. intros. unfold IncidentL in *. replace (P1 (Lin A B H)) with A; trivial. replace (P2 (Lin A B H)) with B; trivial. split;intro. assert (T:=Cond l). elim (eq_dec_points X B); intro. subst X. auto. assert (Col (P1 l) A B). apply col_transitivity_1 with (P2 l); Col. assert (Col (P2 l) A B). apply (col_transitivity_2 (P1 l)); Col. apply (col3 A B); Col. assert (U:=Cond l). apply (col3 (P1 l) (P2 l)); 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