proposition: Lemma drop_seq j n m : drop m (seq j n) = seq (j + m) (n - m).
proof: Proof. revert j m. induction n as [|n IH]; simpl; intros j m. - rewrite drop_nil. done. - destruct m; simpl. + rewrite Nat.add_0_r. done. + rewrite IH. f_equal; lia. Qed.
imports: stdpp(options)