proposition: Lemma map_seqZ_snoc start xs x : map_seqZ start (xs ++ [x]) =@{M A} <[(start + Z.of_nat (length xs)):=x]> (map_seqZ start xs).
proof: Proof. rewrite map_seqZ_app, map_seqZ_singleton. by rewrite insert_union_singleton_r by (by rewrite map_seqZ_snoc_disjoint). Qed.
imports: Coq(Permutation) stdpp(options)