proposition: Lemma zero_ortho_tout : forall A B : PO, orthogonal (vec A B) zero.
proof: Proof. intros A B; try assumption. VReplace zero (vec A A). apply def_orthogonal2. VReplace (vec A A) (mult_PP 0 (vec A B)). Simplscal. Qed.