proposition: Lemma cong2_per2__cong_conga2 : forall A B C A' B' C', A<>B -> B<>C -> Per A B C -> Per A' B' C' -> Cong A C A' C' -> Cong B C B' C' -> Cong B A B' A' /\ CongA B A C B' A' C' /\ CongA B C A B' C' A'.
proof: Proof. intros. assert_diffs. destruct (l11_46 A B C) as [_ []]; auto using per_not_col. apply (l11_52 A B C A' B' C');auto. apply l11_16;auto. intro. subst B'. apply H9, cong_transitivity with A' C'; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2