proposition: Lemma per_perp_in : forall A B C, A <> B -> B <> C -> Per A B C -> Perp_at B A B B C.
proof: Proof. intros. unfold Perp. repeat split. assumption. assumption. Col. Col. intros. eapply per_col. apply H0. eapply l8_2. eapply per_col. intro. apply H. apply sym_equal. apply H4. apply l8_2. assumption. Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR