proposition: Lemma op_leq_weq_2 {h k l X Y Z} {HX: laws h X} {HY: laws k Y} {HZ: laws l Z} {f: X -> Y -> Z} {Hf: Proper (leq ==> leq ==> leq) f}: Proper (weq ==> weq ==> weq) f.
proof: Proof. intros x y E x' y' E'. rewrite weq_spec in E. rewrite weq_spec in E'. apply antisym; apply Hf; (apply E || apply E'). Qed.
imports: common level