proposition: Lemma distinct_egalite_vecteur : forall A B C D : PO, A <> B :>PO -> vec C D = vec A B :>PP -> C <> D :>PO.
proof: Proof. red in |- *; intros. apply H; apply vecteur_nul_conf. rewrite <- H0; rewrite <- H1; Ringvec. Qed.