proposition: Lemma not_archimedes__line_completeness : ~ archimedes_axiom -> line_completeness.
proof: Proof. intros narchi Tm Tm2 P Q f archi Hf. assert (Hf' := Hf). destruct Hf' as [HPQ [finj [fBet fCong]]]. assert (Haux := col2_diff_inj_line__diff f P Q finj). exfalso. apply narchi, (archimedes_aux P Q). intros R S HR HS HQR. remember (f Q) as Q'. remember (f R) as R'. remember (f S) as S'. destruct (archi Q' R' Q' S') as [R0' [HGrad HLe]]. subst; intro; apply HQR, finj; Col. assert (HBet : Bet Q' S' R0'). { destruct (eq_dec_points Q S); [subst; Between|]. apply l6_13_1; trivial. apply l6_7 with R'; subst. apply l6_2 with (f P); Col; apply fBet; Between; Col. apply bet_out; Col; apply grad__bet, HGrad. } clear HLe. revert S S' HeqS' HS HBet. induction HGrad; intros; subst. { exists R; split; [apply grad_init|]. apply bet__le1213, (line_extension_reverse_bet f P Q); Col. } rename C into C0'. destruct (eq_dec_points Q S). subst; exists R; split; [apply grad_init|apply le_trivial]. assert (Hd : Bet (f Q) (f S) C0' \/ Bet (f Q) C0' (f S)). { destruct (eq_dec_points C0' (f Q)); [subst; Between|]. apply l6_7 with C'. apply bet_out; Col. apply l6_6, bet_out; Col. } destruct Hd; [apply IHHGrad with (f S); trivial|]. assert (HS0 : exists S0, Bet Q S0 S /\ Cong S S0 Q R). { apply segment_reverse, (line_extension_reverse_bet f P Q); Col. apply between_exchange4 with C0'; Between. } destruct HS0 as [S0 []]. assert (S <> S0) by (intro; treat_equalities; auto). assert (HC0 : Reach Q R Q S0). { assert (Bet P Q S0) by (apply between_inner_transitivity with S; assumption). apply IHHGrad with (f S0); trivial. apply between_inner_transitivity with (f S); Col. destruct (eq_dec_points C0' (f S)); [subst; Between|]. apply between_symmetry, l6_13_1. apply bet2__out with (f Q); try apply between_symmetry; Col. apply (l5_6 (f S) C0' C0' C'). apply le_left_comm, bet__le1213, (between_exchange3 (f Q)); assumption. Cong. apply cong_symmetry, cong_transitivity with (f Q) (f R); Col. } clear IHHGrad. destruct HC0 as [C0 []]. destruct (segment_construction Q C0 Q R) as [C []]. exists C; split; [apply grad_stab with C0; Cong|]. apply bet__le1213. destruct (eq_dec_points Q S0). { subst S0; assert (R = S) by (apply (between_cong_3 P Q); Cong). treat_equalities; apply between_exchange4 with C0; Between. } assert (Bet Q S0 C0). { apply l6_13_1; trivial. apply l6_7 with S; [Out|]. apply l6_7 with R. apply l6_2 with P; Between. apply bet_out; Between. } apply outer_transitivity_between2 with S0; auto. assert (Bet Q S0 C) by (apply between_exchange4 with C0; assumption). apply l6_13_1. apply l6_2 with Q; Between; intro; treat_equalities; auto. apply le_right_comm; exists C0; split. apply between_inner_transitivity with Q; Between. apply cong_transitivity with Q R; Cong. 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