* Lower_Bound: proved with GNATProve GPL2014, one sucpicious
          invariant to be investigated