proposition: Lemma flip_invol {x y} (f h : x ~> y) (g : y ~> y) `{@Involutive _ g} : f ≈ g ∘ h ↔ g ∘ f ≈ h.
proof: Proof. split; intros. - rewrite X, comp_assoc, invol; cat. - rewrite <- X, comp_assoc, invol; cat. Qed.
imports: Category.Lib Category.Theory.Category