proposition: Lemma morph_compose `(tB : t B leB) `(tC : t C leC) : forall (f : A -> B) (g : B -> C), morph le leB f -> morph leB leC g -> morph le leC (fun x => g (f x)).
proof: Proof. unfold morph; auto. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat