proposition: Lemma l2_11_b : 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. apply Cong_stability; intro. assert (A<>B). intro; subst. assert (A'=B') by (apply (cong_identity A' B' B); Cong). subst; tauto. assert (Cong C A C' A') by (apply (five_segment _ _ _ _ _ _ _ _ H1 );auto using cong_trivial_identity, cong_commutativity). apply H3; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong