proposition: Lemma comp_edge_cone_to_limit : forall r s x b, is_limit s -> is_cone r -> socle r = socle s -> b = cone_target s -> ob (cone_source s) x -> comp b (edge s x) (cone_to_limit r s) = edge r x.
proof: Proof. ir. transitivity (edge (cone_compose s (cone_to_limit r s)) x). rw edge_cone_compose. rww H2. am. rww cone_composable_cone_to_limit. rw cone_compose_cone_to_limit. tv. am. am. am. Qed.
imports: Arith nat_trans