proposition: Lemma link_lemma_2 : forall z rz, repr (t[ b>- a]) z rz -> rz<>a -> repr t z rz.
proof: Proof. induction 1; intros. apply rzero. intro; apply H. map_iff; auto. revert H1; map_iff. completer subst. eapply rsucc; eauto. revert H; map_iff; intuition subst. assert (j = r). eapply repr_inj_right. eapply repr_a. eauto. subst. tauto_false. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)