proposition: Lemma per_col_eq : forall A B C, Per A B C -> Col A B C -> B <> C -> A = B.
proof: Proof. intros. unfold Per in H. ex_and H C'. assert_bets. assert_cols. assert (Col A C C') by ColR. assert (C = C' \/ Midpoint A C C') by (eapply l7_20;Col). induction H6. treat_equalities. intuition. eapply l7_17;eauto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar