proposition: Lemma unitaire_distincts : forall A B : PO, scalaire (vec A B) (vec A B) = 1 -> A <> B :>PO.
proof: Proof. intros; unfold not in |- *; intros. absurd (scalaire (vec A B) (vec A B) = 1); auto. rewrite H0. pattern (vec B B) at 1 in |- *. replace (vec B B) with (mult_PP 0 (vec A B)). rewrite scalaire_mult_g. replace (0 * scalaire (vec A B) (vec B B)) with 0. auto with *. ring. unfold vec in |- *; RingPP. Qed.