proposition: Lemma bet_dec_eq_dec_b : (forall A B:Tpoint, ~ A <> B -> A = B).
proof: Proof. intros A B HAB. apply between_identity. apply Bet_stability. intro HNBet. apply HAB. intro HEq. subst. apply HNBet. apply between_trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong