proposition: Lemma diff_per_diff : forall A B P R , A <> B -> Cong A P B R -> Per B A P -> Per A B R -> P <> R.
proof: Proof. intros. intro. subst. assert (A = B). eapply l8_7. apply l8_2. apply H1. apply l8_2. assumption. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR