proposition: Lemma playfair_s_postulateH : playfair_s_postulate.
proof: Proof. intros A1 A2 B1 B2 C1 C2 P HPar1 HCol1 HPar2 HCol2. assert_diffs. destruct (line_existence A1 A2) as [l [Hl1 Hl2]]; auto. destruct (line_existence B1 B2) as [m1 [Hm11 Hm12]]; auto. destruct (line_existence C1 C2) as [m2 [Hm21 Hm22]]; auto. elim (IncidL_dec P l); intro HInc. { assert (Col A1 A2 P) by (apply ColH__Col; exists l; auto). elim HPar1; [unfold Par_strict in *|]; [intros [_ HFalse]; exfalso; apply HFalse; exists P; Col|]; intros [? [? [? ?]]]. elim HPar2; [unfold Par_strict in *|]; [intros [_ HFalse]; exfalso; apply HFalse; exists P; Col|]; intros [? [? [? ?]]]; split; ColR. } { assert (HNC : ~ Col A1 A2 P). { assert (HNC : ~ ColH A1 A2 P). { apply IncidL_not_IncidL__not_colH with l; auto. } intro; apply HNC; apply Col__ColH; auto. } assert (HPara1 : Para l m1). { elim HPar1; [|intros [? [? [? ?]]]; exfalso; apply HNC; ColR]. intros [HCop HFalse]; split. { intros [I [HInc1 HInc2]]; apply HFalse; exists I. split; apply ColH__Col; [exists l|exists m1]; auto. } { destruct HPar1 as [HPar1|[HDiff1 [HDiff2 [HCol3 HCol4]]]]; [|exfalso; apply HNC; ColR]. apply coplanar_plane in HCop. destruct HCop as [p [Hp1 [Hp2 [Hp3 Hp4]]]]; exists p. split; assert_diffs; [apply line_on_plane with A1 A2|apply line_on_plane with B1 B2]; auto. } } assert (HPara2 : Para l m2). { elim HPar2; [|intros [? [? [? ?]]]; exfalso; apply HNC; ColR]. intros [HCop HFalse]; split. { intros [I [HInc1 HInc2]]; apply HFalse; exists I. split; apply ColH__Col; [exists l|exists m2]; auto. } { destruct HPar2 as [HPar2|[HDiff1 [HDiff2 [HCol3 HCol4]]]]; [|exfalso; apply HNC; ColR]. apply coplanar_plane in HCop. destruct HCop as [p [Hp1 [Hp2 [Hp3 Hp4]]]]; exists p. split; [apply line_on_plane with A1 A2|apply line_on_plane with C1 C2]; auto. } } assert (HInc1 : IncidL P m1). { apply Col__ColH in HCol1; destruct HCol1 as [m1' [? [? ?]]]. apply IncidL_morphism with m1'; auto. apply line_uniqueness with B1 B2; Col. } assert (HInc2 : IncidL P m2). { apply Col__ColH in HCol2; destruct HCol2 as [m2' [? [? ?]]]. apply IncidL_morphism with m2'; auto. apply line_uniqueness with C1 C2; Col. } assert (HEq := euclid_uniqueness l P m1 m2 HInc HPara1 HInc1 HPara2 HInc2). split; apply ColH__Col; exists m1; split; auto; apply IncidL_morphism with m2; auto; assert(HH:= EqL_Equiv); destruct HH; apply Equivalence_Symmetric; 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