proposition: Lemma cc_cr_mult_mon : is_CMonoid (Build_CSemiGroup (csg_crr cc_cgroup) _ cc_cr_mult_associative) cc_one.
proof: Proof. apply Build_is_CMonoid. unfold is_rht_unit in |- *. intros. elim x. intros. simpl in |- *. unfold cc_eq in |- *. simpl in |- *. split; rational. unfold is_lft_unit in |- *. intros. elim x. intros. simpl in |- *. unfold cc_eq in |- *. simpl in |- *. split; rational. Qed.
imports: CoRN.reals.NRootIR