proposition: Lemma cong_existence' : forall A B l M, A <> B -> IncidL M l -> exists A' B', IncidL A' l /\ IncidL B' l /\ BetH A' M B' /\ CongH M A' A B /\ CongH M B' A B.
proof: Proof. intros A B l M HAB HInM. assert (H : exists P, IncidL P l /\ M <> P). { destruct (two_points_on_line l) as [P1 [P2 [HP2 [HP1 HP1P2]]]]. elim (eq_dec_pointsH M P1); intro HMP1; try subst P1; [exists P2; auto|]. elim (eq_dec_pointsH M P2); intro HMP2; try subst P2; exists P1; auto. } destruct H as [P [HInP HMP]]. destruct (between_out P M) as [P' HP']; auto. destruct (cong_existence A B M P l) as [A' [HInA' [HoutA' HCongA']]]; auto. destruct (cong_existence A B M P' l) as [B' [HInB' [HoutB' HCongB']]]; auto; [apply betH_distincts in HP'; tauto|apply between_col in HP'| exists A', B'; repeat split; auto; apply betH_outH2__betH with P P'; auto]. destruct HP' as [l' [HIn1 [HIn2 HIn3]]]; apply IncidL_morphism with l'; auto. apply line_uniqueness with M P; auto. Qed.
imports: Setoid Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Axioms.hilbert_axioms