proposition: Lemma Nposmult_is_CSemiGroup : is_CSemiGroup Npos Npos_mult.
proof: Proof. unfold is_CSemiGroup in |- *. unfold associative in |- *. unfold Npos_mult in |- *. simpl in |- *. intros x y z. case x. case y. case z. simpl in |- *. intros a pa b pb c pc. auto with arith. Qed.
imports: CoRN.algebra.CSemiGroups CoRN.model.semigroups.Nsemigroup CoRN.model.setoids.Npossetoid