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