Gödel's speed-up theorem implies that some proofs can get significantly shortened when allowing extra axioms. There are concrete examples of this phenomenon for instance when moving from Peano arithmetic (PA) to PA + consistency(PA), or when moving from PA to second-order arithmetic, see for instance this question.

However, I am not aware of concrete examples of such a dramatic shortening when moving from constructive logic to classical logic.

So, is there a known example of a statement that is both true in constructive and classical logic, that has a reasonably short proof in classical logic, but such that any proof in constructive logic would be gigantic (and thus not "human-readable")?

Ideally, an example would be a statement that would feel "concrete enough" for the average mathematician, i.e. a statement involving numbers, graphs, algebraic structures, etc. (Friedman's examples on Kruskal's tree theorem fit the bill)

(I would also be interested in an example that has a simple proof in classical logic, that is not yet known to be true in constructive logic but such that a proof, if it exists, must be gigantic.)

Update: There are indeed ways to construct such examples as indicated below, but which feel a bit like cheating as they essentially add the extra axiom in the statement. I am more thinking of some existence theorem of the form

"For every object x satisfying ..., there exists an object y satisfying ...".

Think Friedman's examples, Four-Color Theorem, etc. In other words, an existence theorem where every constructive proof would be gigantic, but where there exists a short nonconstructive proof. Here again, one may hack this by artificially adding something of the form "or (A or not(A))" in the statement, but of course that's not really what I have in mind, nor the sort of statement a mathematician working with classical logic would try to prove on a regular day ;-)