proposition: Lemma l8_6 : forall A B C A', Per A B C -> Per A' B C -> Bet A C A' -> B=C.
proof: Proof. unfold Per. intros. ex_and H C'. ex_and H0 C''. assert (C'=C'') by (eapply symmetric_point_uniqueness;eauto). subst C''. assert (C = C') by (eapply l4_19;eauto). subst C'. apply l7_3. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR