proposition: Lemma bet_cong_bet : forall A B C D, A <> B -> Bet A B C -> Bet A B D -> Cong A C B D -> Bet B C D.
proof: Proof. intros. assert(Bet B C D \/ Bet B D C). eapply (l5_2 A); auto. induction H3. assumption. assert(D = C /\ A = B). eapply (bet_cong_eq A B D C); auto. eBetween. Cong. spliter. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel