(- 1) * seq is Cauchy ;
hence - seq is Cauchy by BHSP_1:55; :: thesis: verum