proposition: Lemma iscommisof {X Y : setwithbinop} (f : binopiso X Y) (is : iscomm (@op X)) : iscomm (@op Y).
proof: Proof. apply (iscommmonob (invbinopiso f) is). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions