proposition: Lemma projete_axe : forall A B M H : PO, A <> B :>PO -> H = projete_orthogonal A B M :>PO -> alignes A B M -> H = M :>PO.
proof: Proof. intros. elim (def_projete_orthogonal2 (A:=A) (B:=B) (C:=M) (H:=H)); auto; intros. apply (unicite_projete_orthogonal (A:=A) (B:=B) (C:=M) (H:=H) (H':=M)); auto. VReplace (vec M M) zero. auto with geo. Qed.