proposition: Lemma is_unit_FS_id:(is_unit (FS_as_CSemiGroup X) (FS_id X)).
proof: Proof. unfold is_unit. intros a. set (H:= (id_is_rht_unit X a)). set (H0:= (id_is_lft_unit X a)). split. exact H0. exact H. Qed.
imports: Coq.Arith.Euclid CoRN.model.Zmod.Cmod CoRN.algebra.CSemiGroups CoRN.tactics.csetoid_rewrite CoRN.model.structures.Nsec CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms