Lemma iscommmonob {X Y : setwithbinop} (f : binopmono X Y) (is : iscomm (@op Y)) : iscomm (@op X). Proof. set (axf := pr2 f). simpl in axf. intros a b. apply (invmaponpathsincl _ (pr2 (pr1 f))). rewrite (axf a b). rewrite (axf b a). apply is. Qed.