proposition: Lemma BRabs0_bis x: realp x -> (x = \0r <-> BRabs x = \0r).
proof: Proof. move => pa; split; first by move => ->; rewrite BRabs_0. case/BR_i0P:pa => h; last by rewrite (BRabs_pos h). move: RS0 => rs0. by rewrite (BRabs_negs h) - {1} BRopp_0; apply: BRopp_inj => //;apply:BRms_sBR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)