proposition: Theorem updateEvalZb : forall c : rZ, valRz (evalZ Ar c) = b -> evalZ (updateArray a b pol La Lb Ar) c = samePolRz (evalZ Ar c) (samePolRz pol (rZPlus a)).
proof: Proof. intros c; case c; simpl in |- *. exact updateEvalNb. intros r H'. cut (forall p q : rZ, rZComp (samePolRz p q) = samePolRz (rZComp p) q); [ intros Eq1; rewrite <- Eq1 | intros p q; case p; case q; simpl in |- *; auto with stalmarck ]. apply EqrZComp; auto with stalmarck. apply updateEvalNb; auto with stalmarck. rewrite <- H'; case (evalN Ar r); auto with stalmarck. Qed.