proposition: Lemma cone_composable_rw : forall c u, is_cone c -> mor (cone_target c) u -> target u = vertex c -> cone_composable c u = True.
proof: Proof. ir. uf cone_composable. app iff_eq; ir; try tv. xd. Qed.
imports: Arith nat_trans