Order polynomial of shifted double staircase This question is related to my earlier question looking for posets with product formulas for their order polynomials.
Recall that the order polynomial $\Omega_P(m)$ of a finite poset $P$ is defined by 
$$\Omega_P(m) := \# \textrm{ weakly order preserving maps $P\to \{1,2,\ldots,m\}$}.$$
Now let $\lambda = (n,n-1,n-2,...,1) + (k,k-1,k-2,...,1)$ for $0 \leq k < n$ be a ``shifted double staircase'' shape (see e.g. Figure 6(c) in Stanley's paper "Promotion and Evacuation", which is linked below). And let $P$ be the poset corresponding to $\lambda$ (i.e., the poset on the boxes of $\lambda$ viewed as a shifted shape, with $u \lessdot v$ if the box $v$ is directly right of or directly below the box $u$).
Question: Is it true that for this $P$ we have 
$$\Omega_P(m) = \prod_{1 \leq i \leq j \leq n} \frac{(m+i+j-2)}{(i+j-1)}\cdot \prod_{1 \leq i \leq j \leq k} \frac{(m+i+j-1)}{(i+j)}?$$
Testing some small cases it looks like this formula works, and this is not an example I have seen in the literature (but a pointer to a place where it is addressed would also definitely be appreciated!).
For context, let me explain some similar formulas which are known.
If $P$ is the poset associated to the (unshifted) staircase $\lambda = (n,n-1,n-2,...,1)$ (this poset is also the Type A root poset), then
$$\Omega_{P}(m) = \prod_{1\leq i \leq j \leq n} \frac{i+j+2m-2}{i+j}.$$
While if $P$ is the poset associated to the shifted staircase $\lambda = (n,n-1,n-2,...,1)$ (this poset is the Type B/D minuscule poset), then
$$\Omega_P(m) = \prod_{1 \leq i \leq j \leq n} \frac{(m+i+j-2)}{(i+j-1)}.$$
Both of these formulas can be seen for instance in the paper "New Symmetric Plane Partition Identities from Invariant Theory Work of De Concini and Procesi
" by Proctor (linked below). Note that the shifted staircase is just the case $k=0$ of the shifted double staircase and the conjectured formula agrees with the known formula in this case. The formula for the case $k=n-1$ is also known: in this case the poset is the Type B root poset; see for instance the abstract by Hamaker and Williams linked below. 
Hamaker, Zachary; Williams, Nathan, Subwords and plane partitions, Proceedings of the 27th international conference on formal power series and algebraic combinatorics, FPSAC 2015, Daejeon, South Korea, July 6–10, 2015. Nancy: The Association. Discrete Mathematics & Theoretical Computer Science (DMTCS). Discrete Mathematics and Theoretical Computer Science. Proceedings, 241-252 (2015). ZBL1335.05177.
Proctor, Robert A., New symmetric plane partition identities from invariant theory work of De Concini and Procesi, Eur. J. Comb. 11, No. 3, 289-300 (1990). ZBL0726.05008.
Stanley, Richard P., Promotion and evacuation, Electron. J. Comb. 16, No. 2, Research Paper R9, 24 p. (2009). ZBL1169.06002.  
 A: Tri Lai and I proved this conjecture, using the techniques from the theory of lozenge tilings. Indeed, this result is almost already proved by Ciucu in https://arxiv.org/abs/1906.02021. We just need to allow slightly more general parameters for the "flashlight" region of the triangular lattice which he considers- and the techniques he developed there suffice to do that. What we are able to show specifically is that for the region: 
the number of lozenge tilings of $F(x,y,z,t)$ is
$$ \prod_{1\leq i \leq j\leq y+z}\frac{x+i+j-1}{i+j-1}\prod_{1\leq i \leq j \leq z} \frac{x+i+j}{i+j} \prod_{i=1}^{t}\prod_{j=1}^{z}\frac{(x+z+2i+j)}{(x+2i+j-1)}.$$
The case $t=0$ corresponds to the order polynomial for the shifted double staircase (where $y+z=n$, $z=k$, and $x=m-1$ in the notation of the original question).
EDIT: The paper with the details is now on the arXiv: https://arxiv.org/abs/2007.05381.
EDIT 2: Soichi Okada has proved an algebraic extension of the SDS order polynomial product formula in: https://arxiv.org/abs/2009.14037.
