proposition: Lemma O_as_rht_unit : is_rht_unit (S:=nat_as_CSetoid) plus_is_bin_fun 0.
proof: Proof. red in |- *. simpl in |- *. intro x. symmetry in |- *. apply plus_n_O. Qed.
imports: CoRN.model.semigroups.Nsemigroup CoRN.algebra.CMonoids