proposition: Lemma per_dec : forall A B C, Per A B C \/ ~ Per A B C.
proof: Proof. intros. unfold Per. elim (symmetric_point_construction C B);intros C' HC'. elim (cong_dec A C A C');intro. left. exists C'. intuition. right. intro. decompose [ex and] H0;clear H0. assert (C'=x) by (apply symmetric_point_uniqueness with C B;assumption). subst. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR