Decidable equality for real numbers (analytic WLPO) implies equinumerosity of open and closed intervals

[jkingdon]

In iset.mm notation:

|- ( A x e. RR A. y e. RR DECID x =/= y -> ( 0 [,] 1 ) ~~ ( 0 (,) 1 )

This is described as "quite clear" in https://mathstodon.xyz/@andrejbauer/112596897981113450 although at least to my eyes I'm not sure I know how to prove it (using just decidable equality of reals, not something stronger like real trichotomy, LPO, countable choice, etc). There are a lot of explicit bijections between an open and closed interval given at places like:

• https://math.stackexchange.com/questions/1201328/bijection-between-open-and-closed-interval
• https://planetmath.org/BijectionBetweenClosedAndOpenInterval
• https://math.stackexchange.com/questions/160738/how-to-define-a-bijection-between-0-1-and-0-1
• https://planetmath.org/openandclosedintervalshavethesamecardinality and
• https://math.stackexchange.com/questions/28568/bijection-between-an-open-and-a-closed-interval

and to define those functions, and show they are bijections, did not look easy (given just decidable equality of reals) unless I was missing something about how it can be done.