proposition: Theorem updateEvalNb : forall c : rNat, valRz (evalN Ar c) = b -> evalN (updateArray a b pol La Lb Ar) c = samePolRz (evalN Ar c) (samePolRz pol (rZPlus a)).
proof: Proof. intros c; unfold evalN in |- *. CaseEq (rArrayGet vM Ar c); simpl in |- *. intros r; case r; simpl in |- *. intros r0 H' H'0; replace c with (valRz (rZPlus c)); auto with stalmarck. rewrite (updateArrayInb a b pol La Lb Ar) with (c := rZPlus c); auto with stalmarck. replace (rZPlus c) with (samePol (rZPlus r0) c); auto with stalmarck. apply wfPcc2 with (Ar := Ar); auto with stalmarck. rewrite H'0; auto with stalmarck. intros r0 H' H'0; replace c with (valRz (rZMinus c)); auto with stalmarck. rewrite (updateArrayInb a b pol La Lb Ar) with (c := rZMinus c); auto with stalmarck. replace (rZMinus c) with (samePol (rZMinus r0) c); auto with stalmarck. apply wfPcc2 with (Ar := Ar); auto with stalmarck. rewrite H'0; auto with stalmarck. intros l H' H'0; rewrite H'0. rewrite (updateArrayb a b pol La Lb Ar); auto with stalmarck. Qed.