proposition: Lemma col_per_perp : forall A B C D, A <> B -> B <> C -> D <> B -> D <> C -> Col B C D -> Per A B C -> Perp C D A B.
proof: Proof. intros. apply per_perp_in in H4. apply perp_in_perp_bis in H4. induction H4. apply perp_distinct in H4. spliter. absurde. eapply (perp_col _ B). auto. apply perp_sym. apply perp_right_comm. assumption. apply col_permutation_4. assumption. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR