proposition: Lemma l8_14_1 : forall A B, ~ Perp A B A B.
proof: Proof. intros. unfold Perp. intro. ex_and H X. unfold Perp_at in H0. spliter. assert (Per A X A). apply H3. Col. Col. assert (A = X). apply (l8_7 A). apply l8_2. apply l8_5. assumption. assert (Per B X B) by (apply H3;Col). assert (B = X). apply l8_7 with B. apply l8_2. apply l8_5. assumption. apply H0. congruence. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR