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