proposition: Lemma D_link_ex : forall x n, D t x n -> exists2 m, D (t [a>-b]) x m & m <= S n.
proof: Proof. induction 1. destruct (eq_num_dec i a). subst. exists 1. apply (DS _ _ b). map_iff. auto. apply DO. map_iff; intros [H' | H']; subst. tauto_false. revert H'. eapply repr_inv_In. eauto. lia. exists O. apply DO. map_iff. intros [H' | H']; subst; tauto_false. lia. destruct (eq_num_dec i a). subst. exists 1. apply (DS _ _ b). map_iff. auto. apply DO. map_iff. intros [H' | H']. subst. tauto_false. revert H'. eapply repr_inv_In. 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)