proposition: Lemma are_inverse_cone_to_limit : forall a b c, is_limit a -> is_limit b -> socle a = socle b -> cone_target a = c -> are_inverse c (cone_to_limit a b) (cone_to_limit b a).
proof: Proof. ir. assert (cone_target b = c). uf cone_target. wr H1. am. cp H; cp H0. uh H4; uh H5; ee. uh H4; uh H5. ee. uhg; ee; try am. app mor_cone_to_limit. sy; am. app mor_cone_to_limit. sy; am. sy; am. rww source_cone_to_limit. rww target_cone_to_limit. sy; am. rww target_cone_to_limit. rww source_cone_to_limit. sy; am. rw source_cone_to_limit. app comp_cone_to_limit_inversely. am. am. sy; am. rww comp_cone_to_limit_inversely. rww source_cone_to_limit. sy; am. Qed.
imports: Arith nat_trans