take INT.Ring ; :: thesis: INT.Ring is strict
thus INT.Ring is strict ; :: thesis: verum