proposition: Theorem Zlt_left n m : n < m -> 0 <= m + -1 + - n.
proof: Proof. intros. rewrite Z.add_shuffle0. change (-1) with (- Z.succ 0). now apply Z.le_0_sub, Z.le_succ_l, Z.lt_0_sub. Qed.
imports: Arith_base BinInt Zorder Decidable Peano_dec Compare_dec