proposition: Lemma l2_11 : forall A B C A' B' C', Bet A B C -> Bet A' B' C' -> Cong A B A' B' -> Cong B C B' C' -> Cong A C A' C'.
proof: Proof. intros. induction (eq_dec_points A B). subst B. assert (A' = B') by (apply (cong_identity A' B' A); Cong). subst; Cong. apply cong_commutativity; apply (five_segment A A' B B' C C' A A'); Cong. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish