proposition: Lemma D_succ : forall x y n, NumMap.MapsTo x y t -> D t x n -> exists2 m, D t y m & n = S m.
proof: Proof. intros x y n H. inversion_clear 1. firstorder. find_tac. exists n0; firstorder. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)