proposition: Lemma between_identity_B : forall A B, ~ BetH A B A.
proof: Proof. intros A B HNBet. unfold BetH in *. destruct HNBet as [HBet [HAB HBA]]. apply between_identity in HBet. subst. intuition. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality