proposition: Theorem updateEvalZab : evalZ (updateArray a b pol La Lb Ar) (rZPlus a) = samePolRz pol (evalZ (updateArray a b pol La Lb Ar) (rZPlus b)).
proof: Proof. simpl in |- *; auto with stalmarck. exact updateEvalNab. Qed.