proposition: Lemma nsteps_add_inv n m x z : nsteps R (n + m) x z → ∃ y, nsteps R n x y ∧ nsteps R m y z.
proof: Proof. revert x. induction n as [|n IH]; intros x Hx; simpl; [by eauto|]. inv Hx; naive_solver. Qed.
imports: stdpp(options)