Lemma isldistrmonob {X Y : setwith2binop} (f : twobinopmono X Y) (is : isldistr (@op1 Y) (@op2 Y)) : isldistr (@op1 X) (@op2 X). Proof. set (ax1f := pr1 (pr2 f)). set (ax2f := pr2 (pr2 f)). intros a b c. apply (invmaponpathsincl _ (pr2 (pr1 f))). change ((pr1 f) (op2 c (op1 a b)) = (pr1 f) (op1 (op2 c a) (op2 c b))). rewrite (ax2f c (op1 a b)). rewrite (ax1f a b). rewrite (ax1f (op2 c a) (op2 c b)). rewrite (ax2f c a). rewrite (ax2f c b). apply is. Qed.