Commit 2021-06-25 18:48 6666ba2f

fix(real/sign): make real.sign 0 = 0 to match int.sign 0 (#8080) Previously sign 0 = 1 which is quite an unusual definition. This definition brings things in line with int.sign, and include a proof of this fact. A future refactor could probably introduce a sign for all rings with a partial order