proposition: Lemma intro_unit_R x y : y * x = 1 /\ x * y = 1 -> unit_R x.
proof: Proof. move=> [yx_eq1 _]; apply: contra_eqN yx_eq1 => /eqP->. by rewrite Rmult_0_r eq_sym R1_neq_0. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun Zwf Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def Rtrigo1 Reals mathcomp(all_ssreflect ssralg poly mxpoly ssrnum) HB(structures)