It is well known that Heisenberg groups cannot be bi-Lipschitz embedded into Euclidean spaces. A standard proof uses the fact that a Lipschitz mapping from a Heisenberg group into a Euclidean space is almost everywhere Pansu differentiable. Do you know proofs of this result that do not use Pansu differentiability? I have heard that there are such proofs, but I do not know where to find them.

EDIT: I like all three answers of rob, Robert Young and YCor so I cannot accept any of them since I would like to accept each of them.