Description: Lemma for taupi . The smallest positive real whose cosine is one is at most 2 x. _pi . (Contributed by Jim Kingdon, 19-Feb-2019) (Revised by AV, 1-Oct-2020)