proposition: Lemma morph_compose {A B C OA OB OC} (tA : t A OA) (tB : t B OB) (tC : t C OC) : forall f g, morph OA OB f -> morph OB OC g -> morph OA OC (fun x => g (f x)).
proof: Proof. intros. constructor; intros. - eapply PO.morph_compose; eapply f_PO; eassumption. - rewrite <- (f_max H0). rewrite (f_eq H0). reflexivity. apply (f_max H). Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat