Readable signature
ModEq(m,a,b)Exact expansion
exists u v. a + m * u = b + m * vThis node is conservative notation, not a theorem, new axiom, predicate constant, or kernel rule. Its expansion is checked for exact first-order AST equivalence.
Definition neighborhood
Expands using
none
Used by definitions
none
Used by theorem statements or local proof propositions
BT003O mod_eq_refl BT003Q mod_eq_trans BT003R mod_eq_add BT003S mod_eq_mul_right BT003T mod_eq_mul_left BT003W mod_eq_bounded_unique BT003X mod_eq_to_remainder_decomposition BT0045 beta_at_of_mod_eq_bound BT0046 dvd_to_mod_zero BT004C bezout_mod_left BT004D bezout_mod_right BT004E mod_eq_predecessor_cancel BT004F binary_crt BT004T mod_eq_of_mod_eq_multiple BT004U binary_crt_fold_step BT005A beta_exclusive_recode_congruence_step BT005B beta_exclusive_recode_invariant_step BT005C bounded_beta_exclusive_recode_invariant BT005D beta_prefix_extend