Exact expanded PA statement
forall n m. n * m = m * nStructural proof guide
Generated structural guide
Multiplication is commutative.
Use the direct prerequisites mul_zero_left, mul_succ_left as previously established PA formulas.
The proof proceeds by structural induction (1), certified simplification (2).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
PA000I bounded_common_multiple_step PA000T right_factor_divides_product PA0015 beta_modulus_coprime_base PA0016 add_mul PA001N balanced_combination_scale_right PA001Q beta_moduli_coprime_of_gap_dvd PA0020 mod_eq_mul_left PA0026 binary_crt PA0029 beta_at_exists PA002F beta_at_unique PA002V mod_eq_to_remainder_decomposition PA003C remainder_decomposition_to_mod_eq PA003Q coprime_mod_inverse PA003R mod_eq_cancel_coprime PA0052 beta_product_replace_balance PA005K mod_eq_decidable_nonzero PA005N square_decomp PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA006C mul_double_right PA0072 gauss_half_range_signed_choices PA007N beta_product_pointwise_mul_exact PA007P gauss_signed_pointwise_mul_scale_mod PA007Q beta_product_pointwise_scale_mod PA0084 gauss_signed_products_cancel_mod PA0086 nondivisor_canonical_remainder_exists PA008A mod_eq_zero_to_dvd_nonzero PA008B prime_mul_index_map_exists_up_to PA008L fermat_predecessor_exponent_mod_one PA008N scaled_inverse_from_unit_inverse PA008Q prime_scaled_inverse_exists PA009B scaled_inverse_symmetric PA00AJ inverse_index_symmetric PA00BN bounded_euler_criterion_dichotomy PA00BO double_predecessor_ne_one PA00BV arbitrary_gauss_lemma_complete PA00C3 odd_half_positive_complement_exists PA00C5 canonical_remainder_from_mod PA00CL odd_reflected_remainder_mod_two PA00DQ odd_half_cross_product_gap PA00ES eisenstein_zero_width_rectangle_sum_zero PA00FK mod_two_one_to_oddFormal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.