proposition: Lemma Bet_sym : forall A B C, Bet A B C -> Bet C B A.
proof: Proof. intros. unfold Bet in *. decompose [or] H. left. eauto using axiom_betweennesssymmetry. right;right;auto. right;left;auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Elements.OriginalProofs.proposition_01 GeoCoq.Elements.OriginalProofs.lemma_congruenceflip GeoCoq.Elements.OriginalProofs.lemma_extension Classical