fact: Definition one_ops : Ops True := {| le := fun _ _ => True ; eq := fun _ _ => True ; max := fun _ _ => I ; min := fun _ _ => I |}.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat