proposition: Lemma update_In : forall i a b, repr t a b -> a <> b -> ~NumMap.In i t -> ~NumMap.In i (t [a >- b]).
proof: Proof. clear. intros. map_iff. intros [H' | H']. subst. revert H. apply repr_zero_inv; auto. tauto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)