proposition: Lemma invertible_commutation_is_limit_cone_pushdown : forall c, target f = c -> invertible c commutation = is_limit (cone_pushdown f a).
proof: Proof. ir. wr H. ap iff_eq; ir. wr cone_compose_commutation. app is_limit_cone_compose. ap cone_composable_commutation. rww cone_target_b. uf commutation. ap invertible_cone_to_limit. am. am. rww socle_cone_pushdown. rww cone_target_cone_pushdown. Qed.
imports: Arith nat_trans