proposition: Lemma cone_to_limit_refl : forall a, is_limit a -> cone_to_limit a a = id (cone_target a) (vertex a).
proof: Proof. ir. transitivity (comp (cone_target a) (cone_to_limit a a) (cone_to_limit a a)). wr cone_to_limit_cone_compose. rw cone_compose_cone_to_limit. tv. lu. am. tv. lu. rww cone_composable_cone_to_limit. lu. tv. rww comp_cone_to_limit_inversely. Qed.
imports: Arith nat_trans