proposition: Lemma D_update_ex : forall x n, D t x n -> exists2 m, D (t [a>-b]) x m & m <= n.
proof: Proof. induction 1. exists O; auto using DO. destruct (eq_num_dec i a). subst. exists (S O). apply (DS _ _ b). map_iff. auto. apply DO. eauto. lia. destruct (IHD). exists (S x). eapply DS. 2 : eauto. map_iff. auto. lia. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)