proposition: Lemma nested__diff : forall A B n m An Bm, Nested A B -> A n An -> B m Bm -> An <> Bm.
proof: Proof. intros A B n m An Bm HAB HAn HBm. destruct (Nat.lt_trichotomy n m) as [Hlt|[Heq|Hlt]]. - destruct (nested__ex_left A B m HAB) as [Am]. apply bet_neq23__neq with Am. apply (nested__bet A B n m m); eassumption. eapply nested__diff0; eassumption. - subst; eapply nested__diff0; eassumption. - destruct (nested__ex_right A B n HAB) as [Bn]. apply nested_sym in HAB. apply not_eq_sym, bet_neq23__neq with Bn. apply (nested__bet B A m n n); assumption. eapply nested__diff0; eassumption. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch07_midpoint Arith