proposition: Lemma nested__ex_left : forall A B n, Nested A B -> exists An, A n An.
proof: Proof. intros A B n [Hex _]. destruct (Hex n) as [An [_ [HAn _]]]. exists An. apply HAn. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch07_midpoint Arith