proposition: Lemma axiom_hcong_1_existence : forall A B A' P l, A <> B -> A' <> P -> IncidentL A' l -> IncidentL P l -> exists B', IncidentL B' l /\ outH A' P B' /\ Cong A' B' A B.
proof: Proof. intros; destruct (l6_11_existence A' A B P) as [B' [HOut HCong]]; auto. exists B'; repeat split; try apply out_outH, l6_6; auto; unfold IncidentL in *. destruct l; simpl in *; ColR. 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