proposition: Lemma line_completeness_aux : line_completeness -> forall (Tm: Tarski_neutral_dimensionless) (Tm2 : Tarski_neutral_dimensionless_with_decidable_point_equality Tm) (f : @Tpoint Tn -> @Tpoint Tm), @archimedes_axiom Tm -> extension f -> forall A P Q R, ~ Col P Q R -> Coplanar (f P) (f Q) (f R) A -> exists B, Coplanar P Q R B /\ f B = A.
proof: Proof. intros lc Tm Tm2 f archi fext A P Q R HNCol HCop. assert (fext' := fext). assert (Haux : forall X Y, X <> Y -> line_extension f X Y). intros; apply extension__line_extension; assumption. unfold extension, inj, pres_bet, pres_cong in fext'; spliter. destruct (@midpoint_existence Tn TnEQD P Q) as [S HS]. assert_diffs. destruct (col_dec (f R) (f S) A). { assert (HB : exists B, Col R S B /\ f B = A). assert (R <> S) by (intro; subst; apply HNCol; Col). apply lc; auto. destruct HB as [B []]. exists B; split; [exists S; left; split|]; Col. } destruct (col_dec (f P) (f Q) A). { assert (HB : exists B, Col P Q B /\ f B = A) by (apply lc; auto). destruct HB as [B []]. exists B; split; Cop. } destruct (hilbert_s_version_of_pasch (f P) (f Q) (f R) A (f S)) as [X [HX1 HX2]]; trivial. repeat split; Between. assert (HY : exists Y, Coplanar P Q R Y /\ f Y = X). { destruct HX2 as [[]|[]]; [assert (HY : exists Y, Col P R Y /\ f Y = X)|assert (HY : exists Y, Col Q R Y /\ f Y = X)]; try apply lc; Col; destruct HY as [Y []]; exists Y; split; Cop. } destruct HY as [Y []]. subst X. assert (S <> Y). { intro; treat_equalities. apply HNCol. apply (extension_reverse_col f); auto. assert (Bet P S Q) by Between. assert (Bet (f P) (f S) (f Q)) by auto. destruct HX2 as [[HBet []]|[HBet []]]; [|apply col_permutation_4]; apply (col_transitivity_2 (f S)); Col. } assert (HB : exists B, Col S Y B /\ f B = A) by (apply lc; Col). destruct HB as [B []]. exists B. split; [apply col_cop2__cop with S Y|]; Cop. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Continuity.grad