proposition: Lemma prop_11 : forall A B C, A <> B -> Col A B C -> exists F, Perp C F A B.
proof: Proof. intros. apply perp_exists; assumption. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions