proposition: Lemma rhtunitNpos : is_rht_unit Npos_mult ONEpos.
proof: Proof. unfold is_rht_unit in |- *. unfold Npos_mult in |- *. intro x. case x. simpl in |- *. intros scs_elem H. auto with arith. Qed.
imports: CoRN.model.semigroups.Npossemigroup CoRN.algebra.CMonoids