proposition: Lemma ligne_niveau_MAMB_O : forall A B M : PO, scalaire (vec M A) (vec M B) = 0 -> cercle_diametre A B M.
proof: Proof. intros. discrimine M A. discrimine M B. apply triangle_rectangle_cercle_diametre; auto with geo. Qed.