proposition: Lemma archimedes_aux : forall P Q, (forall R S, Bet P Q R -> Bet P Q S -> Q <> R -> Reach Q R Q S) -> archimedes_axiom.
proof: Proof. intros P Q Haux A B C D HAB. destruct (segment_construction P Q A B) as [R []]. destruct (segment_construction P Q C D) as [S []]. destruct (Haux R S) as [R' [HGrad HLe]]; Col. intro; treat_equalities; auto. assert (Bet Q R R') by (apply grad__bet, HGrad). assert (HB' : Le A B Q R') by (apply le_transitivity with Q R; Le). apply l5_5_1 in HB'. destruct HB' as [B' []]. exists B'; split. apply (grad2__grad456 Q R R'), bet_cong2_grad__grad2; trivial. apply l4_3_1 with Q A; Cong. apply (l5_6 Q S 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