proposition: Lemma natIso_inv_natural (phi:natIso) {A B} (f : C⦅A ; B⦆) : ni_inv phi ∙ fmap G f ∼ fmap F f ∙ ni_inv phi.
proof: Proof. symmetry. match goal with | [|- ?f ∙ _ ∼ _] => rewrite -(cat_law1 _ _ _ f) end. rewrite -(ni_leftinv phi) -(cat_law3 _ _ _ _ _ _ _ (ni_inv phi)). rewrite ni_natural -!cat_law3 ni_rightinv cat_law2. reflexivity. Qed.
imports: Coq(ssreflect ssrfun) Coq.Relations(Relation_Definitions) Coq.Classes(RelationClasses Morphisms) Mon(SPropBase)