proposition: Lemma midpoint_preserves_bet : forall A B C B' C', Midpoint B' A B -> Midpoint C' A C -> (Bet A B C <-> Bet A B' C').
proof: Proof. intros. split. intro. eapply bet_half_bet. apply H1. assumption. assumption. intro. eapply bet_double_bet. apply H. apply H0. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel