ada: Update contracts on Strings libraries

ada: Update contracts on Strings libraries

The contracts of Ada.Strings.Bounded.To_String and
Ada.Strings.Fixed.Delete are updated to reflect the standard spec and to
allow proof of callers.

gcc/ada/

	* libgnat/a-strbou.ads (To_String): Add a postcondition to state
	the value of bounds of the returned string, which helps with proof
	of callers.
	* libgnat/a-strfix.adb (Delete): Fix implementation to produce
	correct result in all cases. For example, returned string should
	always have a lower bound of 1, which was not respected in one
	case. This was not detected by proof, since this code was dead
	according to the too strict precondition.
	* libgnat/a-strfix.ads (Delete): State the correct precondition
	from standard which allows a value of Through beyond the last
	valid index, and also restricts values of From from below. Update
	the Contract_Cases accordingly to allow new values of parameters.