fact: Definition toJoinLatOps' {A} (ops : Ops A) : JoinLat.Ops A := {| JoinLat.le := le ; JoinLat.eq := eq ; JoinLat.max := max |}.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat