注文まわりで Lean と TLA+ が確かめた性質と、クーポン適用でこれから証明する性質の案です。返金額の上限は、部分返金を繰り返す場合などの証明がまだ終わっていません。クーポンの 3 件は実装に入る前に合意したいので、足りない性質や強すぎる主張があればコメントください。