proposition: Theorem updateArrayOtherwise : forall c : rNat, ~ InRz (rZPlus c) Lb -> c <> a -> c <> b -> rArrayGet _ updateArray c = rArrayGet _ Ar c.
proof: Proof. intros c NotPInb NotEqca NotEqcb. unfold updateArray in |- *. replace c with (valRz (rZPlus c)); auto with stalmarck. rewrite rArrayDef2; auto with stalmarck. rewrite rArraySetListInv1; auto with stalmarck. red in |- *; intros H'. unfold appendRz in H'. case appendfInvEq with (1 := H'); auto with stalmarck; intros H'0; inversion_clear H'0; inversion H; auto with stalmarck. Qed.