fact: Definition pointwise_ops {A B} (O : forall a : A, Ops (B a)) : Ops (forall a, B a) := {| le := pointwise_op (fun a => @le _ (O a)) ; eq := pointwise_op (fun a => @eq _ (O a)) ; min := (fun f g a => @min _ (O a) (f a) (g a)) |}.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat