let i1 be Nat; :: thesis: ( 1 <= i1 implies i1 -' 1 < i1 )
assume A1: 1 <= i1 ; :: thesis: i1 -' 1 < i1
i1 - 1 < i1 - 0 by XREAL_1:15;
hence i1 -' 1 < i1 by A1, XREAL_1:233; :: thesis: verum