proposition: Lemma l4_19 : forall A B C C', Bet A C B -> Cong A C A C' -> Cong B C B C' -> C=C'.
proof: Proof. intros. induction (eq_dec_points A B). treat_equalities; reflexivity. apply (l4_18 A B); Cong. auto using bet_col with col. Qed.
imports: GeoCoq.Tarski_dev.Ch04_cong_bet