proposition: Lemma per_distinct_1 : forall A B C, Per A B C -> B <> C -> A <> C.
proof: Proof. intros. intro. subst C. apply H0. apply eq_sym. apply (l8_8). assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR