Lemma iscommringops_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) : iscommringops op1 op2 → iscommringops (binop_weq_fwd H op1) (binop_weq_fwd H op2). Proof. intro is. split. - apply isringops_weq_fwd, (pr1 is). - apply iscomm_weq_fwd, (pr2 is). Defined.