Commit 2022-08-23 10:32 aeb7facf
View on Github →feat(data/rat/cast): add lemmas, golf (#16194)
- add
rat.cast_strict_mono
,rat.cast_strict_mono
, andrat.cast_order_embedding
; - use these lemmas to prove
rat.cast_le
etc; - add
rat.preimage_cast_Ixx
.