proposition: Lemma eq_transitivity : forall l m n, l =l= m -> m =l= n -> l =l= n.
proof: Proof. unfold EqL,IncidentL. intros. assert (T:=H X). assert (V:= H0 X). split;intro;intuition. 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