proposition: Lemma nested_sym : forall A B, Nested A B -> Nested B A.
proof: Proof. intros A B [Hex HAB]. split; intro n. destruct (Hex n) as [An [Bn []]]; exists Bn, An; split; assumption. intros Bn Bm Am An HBn HBm HAm HAn. destruct (HAB n An Am Bm Bn HAn HAm HBm HBn) as [HBet1 [HBet2 Hd]]. repeat split; Between. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch07_midpoint Arith