proposition: Theorem updateEvalNab : evalN (updateArray a b pol La Lb Ar) a = samePolRz pol (evalN (updateArray a b pol La Lb Ar) b).
proof: Proof. unfold evalN in |- *; rewrite (updateArraya a b pol La Lb Ar); rewrite (updateArrayb a b pol La Lb Ar); auto with stalmarck. case pol; auto with stalmarck. Qed.