proposition: Lemma archimedes_aux : (forall A B C, Out A B C -> Reach A B A C) -> archimedes_axiom.
proof: Proof. intros Haux A B C D HAB. destruct (eq_dec_points C D). subst; exists B. split; Le. apply grad_init. destruct (segment_construction_3 A B C D) as [E [HOut HCong]]; auto. destruct (Haux A B E HOut) as [B' [HGrad HLe]]; trivial. exists B'. split; trivial. apply le_transitivity with A E; Le. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch07_midpoint