proposition: Lemma nested_aux1 : forall A B n m An Am Bm, Nested A B -> n < m -> A n An -> A m Am -> B m Bm -> Bet An Am Bm.
proof: Proof. intros A B n m An Am Bm [Hex HAB] Hcomp. destruct (Hex n) as [_ [Bn [_ HBn]]]. revert Am Bm. induction Hcomp. intros Am Bm HAn HAm HBm. destruct (HAB n An Am Bm Bn); auto. intros Am' Bm' HAn HAm' HBm'. destruct (Hex m) as [Am [Bm []]]. assert (HBet : Bet An Am Bm) by (apply IHHcomp; trivial). destruct (HAB m Am Am' Bm' Bm) as [HBet1 [HBet2 Hd]]; trivial. assert (Bet An Am Bm') by eBetween. clear HBet HBet2; eBetween. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch07_midpoint Arith