Commit 2023-07-25 23:43 4d5aef92

View on Github →

feat: add lemmas about floor/ceil/fract/round and OfNat.ofNat (#6037) Motivated by fract_add_one from the Sphere Eversion Project.

Estimated changes

modified theorem Int.abs_fract
added theorem Int.ceil_add_ofNat
added theorem Int.ceil_ofNat
added theorem Int.ceil_sub_ofNat
added theorem Int.floor_add_ofNat
added theorem Int.floor_ofNat
added theorem Int.floor_ofNat_add
added theorem Int.floor_sub_ofNat
added theorem Int.floor_sub_one
added theorem Int.fract_add_ofNat
added theorem Int.fract_add_one
deleted theorem Int.fract_int_nat
added theorem Int.fract_nat_add
added theorem Int.fract_ofNat
added theorem Int.fract_ofNat_add
added theorem Int.fract_one_add
added theorem Int.fract_sub_ofNat
added theorem Int.fract_sub_one
added theorem Nat.ceil_add_ofNat
added theorem Nat.floor_add_ofNat
added theorem Nat.floor_div_ofNat
added theorem Nat.floor_sub_ofNat
added theorem Nat.floor_sub_one
added theorem round_add_ofNat
added theorem round_ofNat
added theorem round_ofNat_add
added theorem round_sub_ofNat