proposition: Theorem updateEvalZO : forall c : rZ, valRz (evalZ Ar c) <> b -> evalZ (updateArray a b pol La Lb Ar) c = evalZ Ar c.
proof: Proof. intros c; case c; simpl in |- *. exact updateEvalNO. intros r H'; apply EqrZComp; auto with stalmarck. apply updateEvalNO; auto with stalmarck. Contradict H'; rewrite <- H'; case (evalN Ar r); auto with stalmarck. Qed.