proposition: Lemma surjective_f: (surjective f_as_CSetoid_fun).
proof: Proof. unfold surjective. simpl. intro b. elim (is_generated_by b). intros m H. exists m. unfold f. exact H. Qed.
imports: Lia CoRN.algebra.CMonoids CoRN.model.monoids.Nmonoid