proposition: Theorem Zabs_Zs : forall z : Z, (Z.abs (Z.succ z) <= Z.succ (Z.abs z))%Z.
proof: Proof. intros z; case z; auto. simpl in |- *; auto with zarith. repeat rewrite Z.abs_eq; auto with zarith. intros p; rewrite Zabs_eq_opp; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz