proposition: Lemma orthonormal_family_axiom_implies_orth_at2__col : orthonormal_family_axiom -> (forall A B C P Q X, Orth_at X A B C X P -> Orth_at X A B C X Q -> Col P Q X).
proof: Proof. rewrite orthonormal_family_aux. intros up A B C P Q X HP HQ. apply orth_at_chara in HP. apply orth_at_chara in HQ. spliter; clean. destruct (ex_ncol_cop2 A B C X) as [D [E [HD [HE HNCol]]]]. apply up with D E; [Col|apply l8_2..]; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv