nat.cast_sub

Stream: maths

[Yaël Dillies]

docs#nat.cast_sub currently only works for add_group. Can we lower that to has_ordered_sub?

[Yakov Pechersky]

nat.cast is pretty early in hierarchy. Could you just provide a generalizing lemma in the order.sub file?

[Yaël Dillies]

Sure but my question is: Is it even provable?

[Yaël Dillies]

It will have to be a second lemma because there's no order structure in nat.cast.