proposition: Lemma bet_stability : forall A B C, ~ ~ BetH A B C -> BetH A B C.
proof: Proof. intros A B C HNNBet. unfold BetH in *. elim (bet_dec A B C); intro HBet; elim (eq_dec_points A B); intro HAB; elim (eq_dec_points B C); intro HBC. subst. exfalso. apply HNNBet. intro. spliter. intuition. subst. exfalso. apply HNNBet. intro. spliter. intuition. subst. exfalso. apply HNNBet. intro. spliter. intuition. repeat split; assumption. exfalso. apply HNNBet. intro. spliter. contradiction. exfalso. apply HNNBet. intro. spliter. contradiction. exfalso. apply HNNBet. intro. spliter. contradiction. exfalso. apply HNNBet. intro. spliter. contradiction. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality