Library probsa.util.r_mult

Require Export Reals.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop seq.
Import Monoid.

From discprob.prob Require Export prob countable.

Lemma Rmult_eq_compat :
  ∀ r1 r2 r3 r4 : R, (r1 = r2 → r3 = r4 → r1 × r3 = r2 × r4)%R.

Lemma Rmult_associative: associative Rmult.
Lemma Rmult_left_id: left_id R1 Rmult.
Lemma Rmult_right_id: right_id R1 Rmult.
Lemma Rmult_commutative: commutative Rmult.

Canonical Rmult_monoid := Law Rmult_associative Rmult_left_id Rmult_right_id.
Canonical Rmult_comoid := ComLaw Rmult_commutative.