proposition: Lemma pisurdeux_scalaire_nul : forall A B C : PO, image_angle pisurdeux = cons_AV (vec A B) (vec A C) -> scalaire (vec A B) (vec A C) = 0.
proof: Proof. intros. apply def_orthogonal. apply pisurdeux_droit; auto. Qed.