proposition: Lemma nested__diff0 : forall A B, Nested A B -> forall n An Bn, A n An -> B n Bn -> An <> Bn.
proof: Proof. intros A B [Hex HAB]. destruct n. intros A0 B0 HA0 HB0. destruct (Hex 1) as [A1 [B1 []]]. destruct (HAB O A0 A1 B1 B0) as [HBet1 [HBet2 Hdiff]]; trivial. assert (Bet A0 A1 B0) by eBetween. assert_diffs; auto. intros Am Bm HAm HBm. destruct (Hex n) as [An [Bn []]]. destruct (HAB n An Am Bm Bn) as [HBet1 [HBet2 Hdiff]]; trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch07_midpoint Arith