proposition: Lemma col_cong_3_cong_3_eq : forall A B C A' B' C1 C2, A <>B -> Col A B C -> Cong_3 A B C A' B' C1 -> Cong_3 A B C A' B' C2 -> C1 = C2.
proof: Proof. intros A B C A' B' C1 C2 HAB HCol HCong1 HCong2. apply l4_18 with A' B'; try apply l4_13 with A B C; Col; unfold Cong_3 in *; spliter. intro; treat_equalities; intuition. apply cong_transitivity with A C; Cong. apply cong_transitivity with B C; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_cong_bet