proposition: Lemma decidability_of_intersectionH : parallel_postulates.decidability_of_intersection.
proof: Proof. intros A B C D. elim (eq_dec_pointsH A B); intro HAB; subst; [left; exists C; Col|]. elim (eq_dec_pointsH C D); intro HCD; subst; [left; exists A; Col|]. destruct (line_existence A B) as [l [Hl1 Hl2]]; auto. destruct (line_existence C D) as [m [Hm1 Hm2]]; auto. elim (hilbert_axioms.decidability_of_intersection l m). { intros [I [HInc1 HInc2]]; left; exists I; split; apply ColH__Col; [exists l|exists m]; auto. } { intro HFalse; right; intros [I [HCol1 HCol2]]; apply HFalse; exists I. apply Col__ColH in HCol1; apply Col__ColH in HCol2. destruct HCol1 as [l' [? [? ?]]]; destruct HCol2 as [m' [? [? ?]]]. split; [apply IncidL_morphism with l'|apply IncidL_morphism with m']; auto; [apply line_uniqueness with A B|apply line_uniqueness with C D]; 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 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates