proposition: Lemma natIso_inv_natural (phi:natIso) {A B} (f : C⦅A ; B⦆) : ni_inv phi ∙ ofmap G f = ofmap F f ∙ ni_inv phi.
proof: Proof. rewrite -[in RHS](ord_cat_law1 _ _ _ (ofmap _ _)) -(ni_leftinv phi) -(ord_cat_law3 _ _ _ _ _ _ _ (ni_inv phi)) ni_natural -!ord_cat_law3 ni_rightinv ord_cat_law2 //. Qed.
imports: Coq(ssreflect ssrfun) Mon(SPropBase) Coq(RelationClasses Morphisms Relation_Definitions)