proposition: Lemma l8_2 : forall A B C, Per A B C -> Per C B A.
proof: Proof. unfold Per. intros. ex_and H C'. assert (exists A', Midpoint B A A'). apply symmetric_point_construction. ex_and H1 A'. exists A'. split. assumption. eapply cong_transitivity. apply cong_commutativity. apply H0. eapply l7_13. apply H. apply l7_2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR