proposition: Lemma nested__bet : forall A B n n1 m An An1 Bm, Nested A B -> n < n1 -> A n An -> A n1 An1 -> B m Bm -> Bet An An1 Bm.
proof: Proof. intros A B n n1 m An An1 Bm HAB Hlt HAn HAn1 HBm. assert (HBA := nested_sym A B HAB). destruct (Nat.eq_dec n1 m). subst n1; apply (nested_aux1 A B n m); assumption. destruct (nested__ex_right A B n1 HAB) as [Bn1]. assert (Bet An An1 Bn1) by (apply (nested_aux1 A B n n1); assumption). destruct (nat_total_order n1 m) as [Hlt1|Hlt1]; auto. - apply between_inner_transitivity with Bn1; trivial. apply between_symmetry, (nested_aux2 B A n1 m); assumption. - apply outer_transitivity_between with Bn1; trivial. apply between_symmetry, (nested_aux1 B A m n1); assumption. apply (nested__diff0 A B HAB n1); assumption. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch07_midpoint Arith