proposition: Lemma cone_compose_commutation : cone_compose b commutation = cone_pushdown f a.
proof: Proof. uf commutation. rw cone_compose_cone_to_limit. tv. app is_cone_cone_pushdown. am. rww socle_cone_pushdown. Qed.
imports: Arith nat_trans