An effective divisor of degree zero is empty

Unwinding. By [F1] the curve $C$ is an integral $k$-scheme of dimension one, so the divisor formalism of [F2] applies. By [F2] the divisor $D$ has finite support and is written as a finite sum $D={\sum }_x{n}_x[x]$ with integer coefficients; by [F3] effectiveness of $D$ says that all coefficients $n_x$ are nonnegative. The degree is the finite sum ${\mathrm{deg}}_k(D)={\sum }_x{n}_x[\kappa (x):k]$ of [F2].

The residue degrees are positive. For each closed point $x$ of $C$ the residue field $\kappa (x)$ is a finite extension of $k$, so $[\kappa (x):k]={\dim }_k\kappa (x)$ is a positive integer, at least one.

Nonnegativity and vanishing. Apply [F4] to the proper geometrically integral curve $C$ and the effective divisor $D$: the degree ${\mathrm{deg}}_k(D)$ is a nonnegative integer, and ${\mathrm{deg}}_k(D)=0$ if and only if $D=0$. In unfolded terms, each summand $n_x[\kappa (x):k]$ is a product of the nonnegative coefficient of step 1.1 and the positive integer of step 1.2, so the sum is nonnegative and can vanish only when every coefficient vanishes.

The comparison clause. Let $D\le D^{\mathrm{\prime }}$ be effective divisors with ${\mathrm{deg}}_k(D)={\mathrm{deg}}_k(D^{\mathrm{\prime }})$, and put $E:=D^{\mathrm{\prime }}-D$. By [F3] the relation $D\le D^{\mathrm{\prime }}$ says that $E$ has nonnegative coefficients, i.e. $E$ is effective; by the additivity in [F2], ${\mathrm{deg}}_k(E)={\mathrm{deg}}_k(D^{\mathrm{\prime }})-{\mathrm{deg}}_k(D)=0$. Applying step 2.1 to the effective divisor $E$ gives $E=0$, hence $D=D^{\mathrm{\prime }}$.

Conclusion. For every effective divisor $D$ on the proper geometrically integral curve $C$ one has ${\mathrm{deg}}_k(D)\ge 0$ with equality exactly for $D=0$ by step 2.1, and two effective divisors with $D\le D^{\mathrm{\prime }}$ and equal degree coincide by step 3.1. No choice principle is used: only coefficients of a finite sum, integer degrees of finite field extensions and the cited degree-additivity are involved.