proposition: Lemma inverse_colimit_to_cocone : forall a b c, is_colimit a -> is_colimit b -> cosocle a = cosocle b -> cocone_target a = c -> inverse c (colimit_to_cocone a b) = colimit_to_cocone b a.
proof: Proof. ir. cp (are_inverse_colimit_to_cocone H H0 H1 H2). app inverse_eq. Qed.
imports: Arith limits