proposition: Lemma op_pres_Dbrack : bin_op_pres_pred _ Dbrack csg_op.
proof: Proof. unfold bin_op_pres_pred. intros x y. unfold Dbrack. intros Hx Hy. elim Hx. clear Hx. intros lx Hx. elim Hy. clear Hy. intros ly Hy. exists (app lx ly). split. intro a. set (H:= (member_app M a ly lx)). elim H. intros H0 H1. intros H2. set (H3:= (H0 H2)). elim H3. (generalize Hx). intuition. (generalize Hy). intuition. elim Hx. clear Hx. intros Hx1 Hx2. astepr ((cm_Sum lx)[+] y). elim Hy. clear Hy. intros Hy1 Hy2. astepr ( (cm_Sum lx)[+](cm_Sum ly) ). apply cm_Sum_app. 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