Interestingly, constructive mathematics cannot prove that the Cauchy and Dedekind constructions are isomorphic:
"As often happens in an intuitionistic setting, classically equivalent notions fork. Dedekind reals give rise to several demonstrably different collections of reals when only intuitionistic logic is assumed"