proposition: Lemma distance_sym : forall A B : PO, distance A B = distance B A.
proof: Proof. unfold distance in |- *; intros; auto. VReplace (vec B A) (mult_PP (-1) (vec A B)). Simplscal. replace (-1 * -1 * scalaire (vec A B) (vec A B)) with (scalaire (vec A B) (vec A B)); try ring. Qed.