proposition: Lemma is_Rbar_mult_unique (x y z : Rbar) : is_Rbar_mult x y z -> Rbar_mult x y = z.
proof: Proof. unfold is_Rbar_mult ; case: x => [x | | ] ; case: y => [y | | ] ; case: z => [z | | ] //= H ; inversion H => // ; case: Rle_dec H => // H0 ; case: Rle_lt_or_eq_dec => //. Qed.
imports: Coq(Reals ssreflect) Rcomplements