proposition: Theorem updateEvalN2Comp : forall c d : rNat, evalN Ar c = rZComp (evalN Ar d) -> evalN (updateArray a b pol La Lb Ar) c = rZComp (evalN (updateArray a b pol La Lb Ar) d).
proof: Proof. intros c d; case (rNatDec (valRz (evalN Ar c)) b); intros Eqt. rewrite updateEvalNb; auto with stalmarck. case (rNatDec (valRz (evalN Ar d)) b); intros Eqt'. rewrite updateEvalNb; auto with stalmarck. intros H'; rewrite H'; case (evalN Ar d); auto with stalmarck. intros H'; Contradict Eqt'; rewrite <- Eqt; rewrite H'; case (evalN Ar d); auto with stalmarck. rewrite updateEvalNO; auto with stalmarck. case (rNatDec (valRz (evalN Ar d)) b); intros Eqt'. intros H'; Contradict Eqt; rewrite <- Eqt'; rewrite H'; case (evalN Ar d); auto with stalmarck. rewrite updateEvalNO; auto with stalmarck. Qed.