Any constructively valid proof by well-founded induction, specialized to the natural numbers as a particular well-founded set, will be an example. Recall that a set $A$ with a relation < is well-founded if for any $S\subseteq A$, if $(\forall y\lt x)(y\in S) \Rightarrow x\in S$, then $S=A$. A proof by well-founded induction proceeds by proving that the set $S$ of "all $x\in A$ such that blah" satisfies that condition, i.e. that if blah is true for all $y\lt x$, then it is also true for $x$. In classical logic, one can separate out such a proof into "case 1: there are no $y\lt x$" and "case 2: there are some $y\lt x$", but in constructive logic this is not generally possible. (It is still possible in the particular case of strong induction on the naturals, since equality of naturals is decidable.) However, interesting proofs by well-founded induction do still exist constructively.
For example, if $A$ is well-founded, and $B$ is equipped with a function $t\colon P B \to B$, then one can prove by well-founded induction on $A$ that there is a unique function $f\colon A\to B$ defined by well-founded recursion, i.e. such that for all $x\in A$ we have $f(x) = t(\lbrace y\in A f(y) \mid y \in A \wedge y \lt x\rbrace)$. Define an attempt to be a partial function $A\rightharpoonup B$ whose domain is down-closed for < and which satisfies the desired condition insofar as it is defined. We can then prove by well-founded induction that any two attempts are equal on the intersection of their domains, and that for all $x$ there exists an attempt whose domain contains $x$, hence the union of all attempts is the desired function.
In classical logic, where emptiness of a set is decidable, we could separate out the empty set as a special case in this argument (or any other), but it wouldn't gain us anything; it would be just as "non-genuine" as Tran Chieu Minh's construction in the other direction.
