fact: Definition ops : MeetLat.Ops A := {| MeetLat.le := fun x y => eql (dot x y) x ; MeetLat.eq := eql ; MeetLat.min := dot |}.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat