proposition: Lemma cone_composable_cone_to_limit : forall a b, is_cone a -> is_limit b -> socle a = socle b -> cone_composable b (cone_to_limit a b) = True.
proof: Proof. ir. cp (cone_to_limit_pr H H0 H1). ee. app iff_eq; ir; try am. Qed.
imports: Arith nat_trans