for a being non empty at_most_one FinSequence of REAL holds [/(Sum a)\] <= Opt a