proposition: Theorem absolu_Zs : forall z : Z, (0 <= z)%Z -> Z.abs_nat (Z.succ z) = S (Z.abs_nat z).
proof: Proof. intros z; case z. 3: intros p H'; contradict H'; auto with zarith. replace (Z.succ 0) with (Z_of_nat 1). intros H'; rewrite Zabs2Nat.id; simpl in |- *; auto. simpl in |- *; auto. intros p H'; rewrite <- Zpos_succ_morphism; simpl in |- *; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz