lawful-words
Releases (1)
-
0.1.0.0 indexed
Definitions (468)
proof_nat.bend
- law add_comm
- law add_assoc
- law add_left_comm
- law add_swap
- law add_cancel_la + x = a + y gives x = y.
- law add_cancel_rx + a = y + a gives x = y.
- law add_self_rx + y = x gives y = 0.
- law add_eq_zero_lx + y = 0 gives x = 0 (and y = 0).
- law add_eq_zero_r
- law sub_zero
- law sub_add(x + y) - y = x.
- law sub_add_l(y + x) - y = x.
- law mul_zero_r
- law mul_succ_r
- law mul_comm
- law mul_one
- law mul_add
- law mul_add_r
- law mul_assoc
- law dbl_add
- law dbl_dist
- law mul2
- law mul2_r
- law mul_dbl_r
- law mul_dbl_l
- law dbl_inj
- law dbl_ne_odd
- law dbl_zero
- law lt_zero
- law lt_irrefl
- law le_zero_l
- law le_refl
- law lt_succ_iffa < 1 + b is a <= b.
- law le_succ_lt1 + a <= b is a < b.
- law not_lt_lenot (a < b) is b <= a.
- law not_le_ltnot (a <= b) is b < a.
- law lt_to_le
- law le_trans
- law lt_le_trans
- law le_lt_trans
- law lt_trans
- law le_add_ra <= a + k and a <= k + a.
- law le_add_l
- law lt_add_selfb + x is never below b.
- law lt_pos
- law pos_add_l
- law lt_add_lc + a < c + b from a < b (and the same for <=).
- law le_add_mono_l
- law le_add_mono_r
- law lt_add_mono_r
- law le_mul_ra <= b gives a * c <= b * c.
- law le_mul_l
- law le_sub_addk <= m gives k + (m - k) = m.
- law go_eqThe loop of Nat.divmod keeps d * b + r + n, with b = 1 + bp and m + r = bp.
- law go_lt
- law div_moda = (a / b) * b + a % b.
- law mod_lt
- law div_uniqq1 * b + r1 = q2 * b + r2 with r1, r2 < b gives q1 = q2.
- law div_mul_add
- law mod_mul_add
- law mod_small
- law div_small
- law mul_mod
- law div_mul
- law mod_one
- law div_one
- law mod_zero_l
- law div_zero_l
- law mod_add_mulAdding a multiple of x does not change the remainder by x.
- law div_add_mul
- law mod_add_mod_lRemainders inside sums and products.
- law mod_add_mod_r
- law mod_mul_mod_l
- law mod_mul_mod_r
- law mod_mod
- law mod_mod_mul(a % (x * y)) % x = a % x.
- law div_div(a / x) / y = a / (x * y).
- def div_lt.goa < b * c with b > 0 gives a / b < c.
- law div_lt
- law pow_add
- law pow_pos
- law pow2s
- law pow_sub12^(1+j) - 1 = 1 + 2 (2^j - 1).
- def pow_sub1.go
- law pow_one_plus
- law pow_le2^m <= 2^k for m <= k.
- law mod_mod_pow(a % 2^m) % 2^k = a % 2^k for k <= m.
- law le_add_subm <= k + (m - k).
- law eq_comm
- law le_nea <= b and a != b give a + 1 <= b.
- law le_not_lta <= b gives not (b < a).
- law le_sub_ra + c <= x gives c <= x - a.
- def lt_mul_cancel.go8a < 8b gives a < b.
- law lt_mul_cancel