proposition: Theorem Zle_abs : forall p : Z, (p <= Z_of_nat (Z.abs_nat p))%Z.
proof: Proof. intros p; case p; simpl in |- *; auto with zarith; intros q; rewrite inject_nat_convert with (p := Zpos q); lia. Qed.
imports: Reals ZArith List PeanoNat Psatz