fact: Definition morph_pointwise {A B C} `{tC : t C leC eqC} (f : B -> A) : morph (pointwise_op (fun _ => leC)) (pointwise_op (fun _ => eqC)) (pointwise_op (fun _ => leC)) (pointwise_op (fun _ => eqC)) (fun g b => g (f b)).
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat