proposition: Theorem updateEvalNO : forall c : rNat, valRz (evalN Ar c) <> b -> evalN (updateArray a b pol La Lb Ar) c = evalN Ar c.
proof: Proof. intros c; unfold evalN in |- *. case (rNatDec c a); intros Eqa; auto with stalmarck. rewrite Eqa; auto with stalmarck; rewrite (updateArraya a b pol La Lb Ar); rewrite geta; auto with stalmarck. case (rNatDec c b); intros Eqb; auto with stalmarck. rewrite Eqb; auto with stalmarck; rewrite (updateArrayb a b pol La Lb Ar); auto with stalmarck; rewrite getb; simpl in |- *; intros H'; Contradict H'; auto with stalmarck. case (InRzDec (rZPlus c) Lb); intros InRLb; auto with stalmarck. case (InEqInv (rZPlus c) Lb); auto with stalmarck; intros InRLb'. replace c with (valRz (rZPlus c)); auto with stalmarck; rewrite (wfPcc1 _ War b (rZPlus c) Lb); simpl in |- *; auto with stalmarck. intros H'; case H'; auto with stalmarck. replace c with (valRz (rZMinus c)); auto with stalmarck; rewrite (wfPcc1 _ War b (rZMinus c) Lb); simpl in |- *; auto with stalmarck. intros H'; case H'; auto with stalmarck. rewrite (updateArrayOtherwise a b pol La Lb Ar c); auto with stalmarck. Qed.