proposition: Lemma op_pres_K: bin_op_pres_pred (cm_crr M) K (csg_op (c:=M)).
proof: Proof. unfold K. unfold bin_op_pres_pred. unfold bin_op_pres_pred in op_pres_C. intros x y Cx Cy i. apply op_pres_C. apply Cx. apply Cy. 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