proposition: Lemma nested_aux2 : forall A B n m An Am Bn, Nested A B -> n < m -> A n An -> A m Am -> B n Bn -> Bet An Am Bn.
proof: Proof. intros A B n m An Am Bn HAB Hcomp HAn HAm HBn. destruct (nested__ex_right A B m HAB) as [Bm]. apply outer_transitivity_between with Bm. apply (nested_aux1 A B n m); assumption. apply between_symmetry, (nested_aux1 B A n m); auto using nested_sym. eapply nested__diff0; eassumption. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch07_midpoint Arith