proposition: Lemma dedekind_variant__completeness : dedekind_variant -> line_completeness.
proof: Proof. intros dedekind Tm Tm2 P Q f archi fLineExt A HA. destruct (eq_dec_points (f P) A). subst; exists P; split; Col. assert (HR : exists R, Col P Q R /\ Bet (f P) A (f R)). { destruct (segment_construction (f P) A (f P) A) as [A1 []]. assert_diffs. destruct (extension_image_density P Q f archi fLineExt A A1) as [R [HR1 [HR2 []]]]; Col. apply col_transitivity_1 with A; Col. exists R; split; eBetween. } destruct HR as [R []]. destruct (dedekind (fun X => Col P Q X /\ Bet (f P) (f X) A /\ (f X) <> A) (fun X => Col P Q X /\ Bet (f P) A (f X)) P R) as [B HB]; simpl. - repeat split; finish. - split; assumption. - intros Z HZ. assert (Col P Q Z) by (assert_diffs; apply col_transitivity_1 with R; Col). destruct (eq_dec_points (f Z) A). subst; right; split; Between. assert (HOut : Out (f P) (f Z) A). { apply l6_7 with (f R); [|Out]. destruct HZ as [HZP [HRP Hdij]]. destruct fLineExt as [HPQ [fInj [fBet fCong]]]. repeat split. intro; apply HZP, fInj; Col. intro; apply HRP, fInj; Col. destruct Hdij; [left|right]; apply fBet; Col. } destruct HOut as [_ [_ [|]]]; [left|right]; split; auto. - intros X Y [HX1 [HX2 HX3]] [HY1 HY2]. split. apply (line_extension_reverse_bet f P Q); Col; eBetween. intro; treat_equalities; contradiction. - exists B. assert (HBet : Bet P B R). apply HB; split; Col; Between. assert (Col P Q B). apply col_transitivity_1 with R; Col; intro; treat_equalities; auto. destruct (eq_dec_points (f B) A); [split; assumption|]. exfalso. assert (Hf := fLineExt). destruct Hf as [HPQ [finj [fBet fCong]]]. destruct (extension_image_density P Q f archi fLineExt A (f B)) as [X [HX1 [HX2 [HX3 Habs]]]]; auto. apply (pres_bet_line__col f P Q); Col. destruct (l5_3 (f P) A (f B) (f R)); auto; [apply fBet; Col|apply Habs..]. * apply between_equality with (f P). apply between_symmetry, fBet, HB; try split; Col; Between. apply between_inner_transitivity with (f B); assumption. clear dependent R; eBetween. * apply between_equality with (f P). clear dependent R; eBetween. apply between_exchange3 with (f R); [|apply bet3__bet with A (f B); eBetween]. apply between_symmetry, fBet; Col. apply HB; split; Col. split; trivial. apply between_exchange2 with (f B); Between. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.completeness GeoCoq.Meta_theory.Continuity.grad GeoCoq.Tarski_dev.Ch08_orthogonality