proposition: Lemma seqZ_cons m n : 0 < n → seqZ m n = m :: seqZ (Z.succ m) (Z.pred n).
proof: Proof. intros H. unfold seqZ. replace n with (Z.succ (Z.pred n)) at 1 by lia. rewrite Z2Nat.inj_succ by lia. f_equal/=. rewrite <-fmap_S_seq, <-list_fmap_compose. apply map_ext; naive_solver lia. Qed.
imports: stdpp(options)