proposition: Lemma l8_7 : forall A B C, Per A B C -> Per A C B -> B=C.
proof: Proof. intros. unfold Per in H. ex_and H C'. symmetric A' C A. induction (eq_dec_points B C). assumption. assert (Per C' C A). eapply l8_3. eapply l8_2. apply H0. assumption. unfold Midpoint in H. spliter. unfold Col. left. assumption. assert (Cong A C' A' C'). unfold Per in H4. ex_and H4 Z. assert (A' = Z) by (eapply (symmetric_point_uniqueness A C A');auto). subst Z. Cong. unfold Midpoint in *. spliter. assert (Cong A' C A' C'). eapply cong_transitivity. apply cong_symmetry. apply cong_commutativity. apply H6. eapply cong_transitivity. apply cong_commutativity. apply H1. apply cong_left_commutativity. assumption. assert (Per A' B C). unfold Per. exists C'. unfold Midpoint. repeat split;auto. eapply l8_6. apply H9. unfold Per. exists C'. split. unfold Midpoint;auto. apply H1. Between. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR