proposition: Lemma BetSEq : forall A B C, BetS A B C <-> Bet A B C /\ A <> B /\ A <> C /\ B <> C.
proof: Proof. intros; unfold BetS; split; intro; spliter; repeat split; auto; intro; treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong