proposition: Lemma BRprod_nz_bis x y: realp x -> realp y -> (x *r y = \0r) -> x = \0r \/ y = \0r.
proof: Proof. move => xr yr pz. case: (equal_or_not x \0r) => xnz; first by left. case: (equal_or_not y \0r) => ynz; first by right. by case: (BRprod_nz xr yr xnz ynz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)