proposition: Lemma per_perp : forall A B C, A <> B -> B <> C -> Per A B C -> Perp A B B C.
proof: Proof. intros. apply per_perp_in in H1. eapply l8_14_2_1a with B;assumption. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR