proposition: Lemma nested_bis__nested : forall A B, Nested_bis A B -> Nested A B.
proof: Proof. unfold Nested_bis, Nested; intros; spliter; split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le GeoCoq.Axioms.continuity_axioms Logic.ChoiceFacts