proposition: Theorem Zle_Zabs : forall z : Z, (z <= Z.abs z)%Z.
proof: Proof. intros z; case z; simpl in |- *; red in |- *; simpl in |- *; auto; try (red in |- *; intros; discriminate; fail). intros p; elim p; simpl in |- *; auto; try (red in |- *; intros; discriminate; fail). Qed.
imports: Reals ZArith List PeanoNat Psatz