proposition: Lemma nested__ex_right : forall A B n, Nested A B -> exists Bn, B n Bn.
proof: Proof. intros A B n HAB; apply nested__ex_left with A; apply nested_sym, HAB. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch07_midpoint Arith