Description: ( ( sinx ) / x ) ~> 1 as (real) x ~> 0 . (Contributed by Paul Chapman, 10-Nov-2012) (Proof shortened by Mario Carneiro, 21-May-2014)