Readable signature
DivRem(n,d,q,r)Exact expansion
n = d * q + r /\ exists h. h + S r = dThis node is notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.
Definition neighborhood
Expands using
Used by definitions
Used by theorem statements or local proof propositions
PA001C division_remainder_succ PA001D division_remainder_exists PA001K gcd_balanced_bezout_exists_up_to PA0029 beta_at_exists PA002V mod_eq_to_remainder_decomposition PA0035 gcd_exists_up_to PA005K mod_eq_decidable_nonzero PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA0072 gauss_half_range_signed_choices PA0086 nondivisor_canonical_remainder_exists PA008B prime_mul_index_map_exists_up_to PA008Q prime_scaled_inverse_exists PA00BX beta_division_prefix_extend PA00BY beta_division_prefix_exists PA00CP gauss_eisenstein_prefix_pointwise_mod_two PA00E1 distinct_odd_prime_row_bit_count_equals_decoded_quotient