take InvShift 1 ; :: thesis: InvShift 1 is convergent_to_0
thus InvShift 1 is convergent_to_0 ; :: thesis: verum