proposition: Lemma mult_PP_regulier : forall (k : R) (P Q : PP), k <> 0 -> mult_PP k P = mult_PP k Q -> P = Q :>PP.
proof: Proof. intros k P Q Hk H0. replace P with (mult_PP (/ k) (mult_PP k P)). rewrite H0. FieldPP k. FieldPP k. Qed.