proposition: Lemma symmetry_preserves_bet : forall A B M A' B', Midpoint M A A' -> Midpoint M B B' -> (Bet M A' B' <-> Bet M A B).
proof: Proof. intros. split. apply symmetry_preseves_bet2; assumption. intro. eapply (symmetry_preseves_bet1 A B); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel