proposition: Lemma cong2_per2__cong : forall A B C A' 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'.
proof: Proof. intros. destruct (eq_dec_points B C). treat_equalities; Cong. destruct (eq_dec_points A B). destruct (eq_dec_points A' B'); subst; [Cong|]. assert_diffs. destruct (cong2_per2__cong_conga2 A' B' C' B B C); Cong; Perp. apply cong2_per2__cong_conga2 with C C'; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2