proposition: Lemma between_cong : forall A B C, Bet A C B -> Cong A C A B -> C = B.
proof: Proof. intros. assert (Bet A B C). eapply l4_6 with A C B; unfold Cong_3; repeat split; Cong. eapply between_equality; eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col