hott-reals

readme

The HoTT book reals form an archimedian ordered field

magnitude positivei implies apart from zero

Addition order properties done

Less equal if and only if not less than