proposition: Lemma Nmult_is_CSemiGroup : is_CSemiGroup nat_as_CSetoid mult_as_bin_fun.
proof: Proof. unfold is_CSemiGroup in |- *. unfold associative in |- *. unfold mult_as_bin_fun in |- *. simpl in |- *. auto with arith. Qed.
imports: CoRN.model.setoids.Nsetoid CoRN.algebra.CSemiGroups