GF005A

gaussian_mutual_divisibility_associate

Mutual actual divisibility is witnessed association, with the all-zero case handled explicitly and the nonzero case using real multiplication cancellation.

Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. GDvd(a,b) → GDvd(b,a) → GAssociate(a,b)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

GMul(a,b,c) · 2GDvd(d,z) · 2GAssociate(a,b) · 1

Actual proof prerequisites

eq_decidable · checked external prerequisitegaussian_zero_divides_only_zerogaussian_one_unitgaussian_multiply_one_leftgaussian_zero_validgaussian_multiply_exists · checked external prerequisitegaussian_multiply_input_right_validgaussian_multiply_input_left_validgaussian_multiply_associativegaussian_multiply_cancel_leftgaussian_multiply_one_rightgaussian_multiply_output_transportgaussian_multiply_commutative
Original expanded first-order statement 
forall a b. (exists gr_quotient_mutual_first. (exists ge_first_rp_mutual_firstproduct ge_first_rn_mutual_firstproduct ge_first_ip_mutual_firstproduct ge_first_in_mutual_firstproduct ge_second_rp_mutual_firstproduct ge_second_rn_mutual_firstproduct ge_second_ip_mutual_firstproduct ge_second_in_mutual_firstproduct. ((exists ge_representation_real_code_mutual_firstproductfirst ge_representation_imaginary_code_mutual_firstproductfirst. (((a) = ((ge_representation_real_code_mutual_firstproductfirst) + (ge_representation_imaginary_code_mutual_firstproductfirst)) * S ((ge_representation_real_code_mutual_firstproductfirst) + (ge_representation_imaginary_code_mutual_firstproductfirst)) + ((ge_representation_imaginary_code_mutual_firstproductfirst) + (ge_representation_imaginary_code_mutual_firstproductfirst))) /\ ((exists ge_balance_positive_mutual_firstproductfirstreal ge_balance_negative_mutual_firstproductfirstreal. (((((ge_representation_real_code_mutual_firstproductfirst) = 2 * (ge_balance_positive_mutual_firstproductfirstreal) /\ (ge_balance_negative_mutual_firstproductfirstreal) = 0) \/ exists ge_signed_half_mutual_firstproductfirstrealdecode. (((ge_representation_real_code_mutual_firstproductfirst) = 2 * ge_signed_half_mutual_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_mutual_firstproductfirstreal) = 0) /\ (ge_balance_negative_mutual_firstproductfirstreal) = S ge_signed_half_mutual_firstproductfirstrealdecode))) /\ ((ge_first_rp_mutual_firstproduct) + ge_balance_negative_mutual_firstproductfirstreal = (ge_first_rn_mutual_firstproduct) + ge_balance_positive_mutual_firstproductfirstreal))) /\ (exists ge_balance_positive_mutual_firstproductfirstimaginary ge_balance_negative_mutual_firstproductfirstimaginary. (((((ge_representation_imaginary_code_mutual_firstproductfirst) = 2 * (ge_balance_positive_mutual_firstproductfirstimaginary) /\ (ge_balance_negative_mutual_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_mutual_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_mutual_firstproductfirst) = 2 * ge_signed_half_mutual_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_mutual_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_mutual_firstproductfirstimaginary) = S ge_signed_half_mutual_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_mutual_firstproduct) + ge_balance_negative_mutual_firstproductfirstimaginary = (ge_first_in_mutual_firstproduct) + ge_balance_positive_mutual_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_mutual_firstproductsecond ge_representation_imaginary_code_mutual_firstproductsecond. (((gr_quotient_mutual_first) = ((ge_representation_real_code_mutual_firstproductsecond) + (ge_representation_imaginary_code_mutual_firstproductsecond)) * S ((ge_representation_real_code_mutual_firstproductsecond) + (ge_representation_imaginary_code_mutual_firstproductsecond)) + ((ge_representation_imaginary_code_mutual_firstproductsecond) + (ge_representation_imaginary_code_mutual_firstproductsecond))) /\ ((exists ge_balance_positive_mutual_firstproductsecondreal ge_balance_negative_mutual_firstproductsecondreal. (((((ge_representation_real_code_mutual_firstproductsecond) = 2 * (ge_balance_positive_mutual_firstproductsecondreal) /\ (ge_balance_negative_mutual_firstproductsecondreal) = 0) \/ exists ge_signed_half_mutual_firstproductsecondrealdecode. (((ge_representation_real_code_mutual_firstproductsecond) = 2 * ge_signed_half_mutual_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_mutual_firstproductsecondreal) = 0) /\ (ge_balance_negative_mutual_firstproductsecondreal) = S ge_signed_half_mutual_firstproductsecondrealdecode))) /\ ((ge_second_rp_mutual_firstproduct) + ge_balance_negative_mutual_firstproductsecondreal = (ge_second_rn_mutual_firstproduct) + ge_balance_positive_mutual_firstproductsecondreal))) /\ (exists ge_balance_positive_mutual_firstproductsecondimaginary ge_balance_negative_mutual_firstproductsecondimaginary. (((((ge_representation_imaginary_code_mutual_firstproductsecond) = 2 * (ge_balance_positive_mutual_firstproductsecondimaginary) /\ (ge_balance_negative_mutual_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_mutual_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_mutual_firstproductsecond) = 2 * ge_signed_half_mutual_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_mutual_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_mutual_firstproductsecondimaginary) = S ge_signed_half_mutual_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_mutual_firstproduct) + ge_balance_negative_mutual_firstproductsecondimaginary = (ge_second_in_mutual_firstproduct) + ge_balance_positive_mutual_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_mutual_firstproductoutput ge_representation_imaginary_code_mutual_firstproductoutput. (((b) = ((ge_representation_real_code_mutual_firstproductoutput) + (ge_representation_imaginary_code_mutual_firstproductoutput)) * S ((ge_representation_real_code_mutual_firstproductoutput) + (ge_representation_imaginary_code_mutual_firstproductoutput)) + ((ge_representation_imaginary_code_mutual_firstproductoutput) + (ge_representation_imaginary_code_mutual_firstproductoutput))) /\ ((exists ge_balance_positive_mutual_firstproductoutputreal ge_balance_negative_mutual_firstproductoutputreal. (((((ge_representation_real_code_mutual_firstproductoutput) = 2 * (ge_balance_positive_mutual_firstproductoutputreal) /\ (ge_balance_negative_mutual_firstproductoutputreal) = 0) \/ exists ge_signed_half_mutual_firstproductoutputrealdecode. (((ge_representation_real_code_mutual_firstproductoutput) = 2 * ge_signed_half_mutual_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_mutual_firstproductoutputreal) = 0) /\ (ge_balance_negative_mutual_firstproductoutputreal) = S ge_signed_half_mutual_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_mutual_firstproduct) * (ge_second_rp_mutual_firstproduct))) + (((ge_first_rn_mutual_firstproduct) * (ge_second_rn_mutual_firstproduct))))) + (((((ge_first_ip_mutual_firstproduct) * (ge_second_in_mutual_firstproduct))) + (((ge_first_in_mutual_firstproduct) * (ge_second_ip_mutual_firstproduct))))))) + ge_balance_negative_mutual_firstproductoutputreal = (((((((ge_first_rp_mutual_firstproduct) * (ge_second_rn_mutual_firstproduct))) + (((ge_first_rn_mutual_firstproduct) * (ge_second_rp_mutual_firstproduct))))) + (((((ge_first_ip_mutual_firstproduct) * (ge_second_ip_mutual_firstproduct))) + (((ge_first_in_mutual_firstproduct) * (ge_second_in_mutual_firstproduct))))))) + ge_balance_positive_mutual_firstproductoutputreal))) /\ (exists ge_balance_positive_mutual_firstproductoutputimaginary ge_balance_negative_mutual_firstproductoutputimaginary. (((((ge_representation_imaginary_code_mutual_firstproductoutput) = 2 * (ge_balance_positive_mutual_firstproductoutputimaginary) /\ (ge_balance_negative_mutual_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_mutual_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_mutual_firstproductoutput) = 2 * ge_signed_half_mutual_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_mutual_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_mutual_firstproductoutputimaginary) = S ge_signed_half_mutual_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_mutual_firstproduct) * (ge_second_ip_mutual_firstproduct))) + (((ge_first_rn_mutual_firstproduct) * (ge_second_in_mutual_firstproduct))))) + (((((ge_first_ip_mutual_firstproduct) * (ge_second_rp_mutual_firstproduct))) + (((ge_first_in_mutual_firstproduct) * (ge_second_rn_mutual_firstproduct))))))) + ge_balance_negative_mutual_firstproductoutputimaginary = (((((((ge_first_rp_mutual_firstproduct) * (ge_second_in_mutual_firstproduct))) + (((ge_first_rn_mutual_firstproduct) * (ge_second_ip_mutual_firstproduct))))) + (((((ge_first_ip_mutual_firstproduct) * (ge_second_rn_mutual_firstproduct))) + (((ge_first_in_mutual_firstproduct) * (ge_second_rp_mutual_firstproduct))))))) + ge_balance_positive_mutual_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_mutual_second. (exists ge_first_rp_mutual_secondproduct ge_first_rn_mutual_secondproduct ge_first_ip_mutual_secondproduct ge_first_in_mutual_secondproduct ge_second_rp_mutual_secondproduct ge_second_rn_mutual_secondproduct ge_second_ip_mutual_secondproduct ge_second_in_mutual_secondproduct. ((exists ge_representation_real_code_mutual_secondproductfirst ge_representation_imaginary_code_mutual_secondproductfirst. (((b) = ((ge_representation_real_code_mutual_secondproductfirst) + (ge_representation_imaginary_code_mutual_secondproductfirst)) * S ((ge_representation_real_code_mutual_secondproductfirst) + (ge_representation_imaginary_code_mutual_secondproductfirst)) + ((ge_representation_imaginary_code_mutual_secondproductfirst) + (ge_representation_imaginary_code_mutual_secondproductfirst))) /\ ((exists ge_balance_positive_mutual_secondproductfirstreal ge_balance_negative_mutual_secondproductfirstreal. (((((ge_representation_real_code_mutual_secondproductfirst) = 2 * (ge_balance_positive_mutual_secondproductfirstreal) /\ (ge_balance_negative_mutual_secondproductfirstreal) = 0) \/ exists ge_signed_half_mutual_secondproductfirstrealdecode. (((ge_representation_real_code_mutual_secondproductfirst) = 2 * ge_signed_half_mutual_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_mutual_secondproductfirstreal) = 0) /\ (ge_balance_negative_mutual_secondproductfirstreal) = S ge_signed_half_mutual_secondproductfirstrealdecode))) /\ ((ge_first_rp_mutual_secondproduct) + ge_balance_negative_mutual_secondproductfirstreal = (ge_first_rn_mutual_secondproduct) + ge_balance_positive_mutual_secondproductfirstreal))) /\ (exists ge_balance_positive_mutual_secondproductfirstimaginary ge_balance_negative_mutual_secondproductfirstimaginary. (((((ge_representation_imaginary_code_mutual_secondproductfirst) = 2 * (ge_balance_positive_mutual_secondproductfirstimaginary) /\ (ge_balance_negative_mutual_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_mutual_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_mutual_secondproductfirst) = 2 * ge_signed_half_mutual_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_mutual_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_mutual_secondproductfirstimaginary) = S ge_signed_half_mutual_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_mutual_secondproduct) + ge_balance_negative_mutual_secondproductfirstimaginary = (ge_first_in_mutual_secondproduct) + ge_balance_positive_mutual_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_mutual_secondproductsecond ge_representation_imaginary_code_mutual_secondproductsecond. (((gr_quotient_mutual_second) = ((ge_representation_real_code_mutual_secondproductsecond) + (ge_representation_imaginary_code_mutual_secondproductsecond)) * S ((ge_representation_real_code_mutual_secondproductsecond) + (ge_representation_imaginary_code_mutual_secondproductsecond)) + ((ge_representation_imaginary_code_mutual_secondproductsecond) + (ge_representation_imaginary_code_mutual_secondproductsecond))) /\ ((exists ge_balance_positive_mutual_secondproductsecondreal ge_balance_negative_mutual_secondproductsecondreal. (((((ge_representation_real_code_mutual_secondproductsecond) = 2 * (ge_balance_positive_mutual_secondproductsecondreal) /\ (ge_balance_negative_mutual_secondproductsecondreal) = 0) \/ exists ge_signed_half_mutual_secondproductsecondrealdecode. (((ge_representation_real_code_mutual_secondproductsecond) = 2 * ge_signed_half_mutual_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_mutual_secondproductsecondreal) = 0) /\ (ge_balance_negative_mutual_secondproductsecondreal) = S ge_signed_half_mutual_secondproductsecondrealdecode))) /\ ((ge_second_rp_mutual_secondproduct) + ge_balance_negative_mutual_secondproductsecondreal = (ge_second_rn_mutual_secondproduct) + ge_balance_positive_mutual_secondproductsecondreal))) /\ (exists ge_balance_positive_mutual_secondproductsecondimaginary ge_balance_negative_mutual_secondproductsecondimaginary. (((((ge_representation_imaginary_code_mutual_secondproductsecond) = 2 * (ge_balance_positive_mutual_secondproductsecondimaginary) /\ (ge_balance_negative_mutual_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_mutual_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_mutual_secondproductsecond) = 2 * ge_signed_half_mutual_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_mutual_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_mutual_secondproductsecondimaginary) = S ge_signed_half_mutual_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_mutual_secondproduct) + ge_balance_negative_mutual_secondproductsecondimaginary = (ge_second_in_mutual_secondproduct) + ge_balance_positive_mutual_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_mutual_secondproductoutput ge_representation_imaginary_code_mutual_secondproductoutput. (((a) = ((ge_representation_real_code_mutual_secondproductoutput) + (ge_representation_imaginary_code_mutual_secondproductoutput)) * S ((ge_representation_real_code_mutual_secondproductoutput) + (ge_representation_imaginary_code_mutual_secondproductoutput)) + ((ge_representation_imaginary_code_mutual_secondproductoutput) + (ge_representation_imaginary_code_mutual_secondproductoutput))) /\ ((exists ge_balance_positive_mutual_secondproductoutputreal ge_balance_negative_mutual_secondproductoutputreal. (((((ge_representation_real_code_mutual_secondproductoutput) = 2 * (ge_balance_positive_mutual_secondproductoutputreal) /\ (ge_balance_negative_mutual_secondproductoutputreal) = 0) \/ exists ge_signed_half_mutual_secondproductoutputrealdecode. (((ge_representation_real_code_mutual_secondproductoutput) = 2 * ge_signed_half_mutual_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_mutual_secondproductoutputreal) = 0) /\ (ge_balance_negative_mutual_secondproductoutputreal) = S ge_signed_half_mutual_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_mutual_secondproduct) * (ge_second_rp_mutual_secondproduct))) + (((ge_first_rn_mutual_secondproduct) * (ge_second_rn_mutual_secondproduct))))) + (((((ge_first_ip_mutual_secondproduct) * (ge_second_in_mutual_secondproduct))) + (((ge_first_in_mutual_secondproduct) * (ge_second_ip_mutual_secondproduct))))))) + ge_balance_negative_mutual_secondproductoutputreal = (((((((ge_first_rp_mutual_secondproduct) * (ge_second_rn_mutual_secondproduct))) + (((ge_first_rn_mutual_secondproduct) * (ge_second_rp_mutual_secondproduct))))) + (((((ge_first_ip_mutual_secondproduct) * (ge_second_ip_mutual_secondproduct))) + (((ge_first_in_mutual_secondproduct) * (ge_second_in_mutual_secondproduct))))))) + ge_balance_positive_mutual_secondproductoutputreal))) /\ (exists ge_balance_positive_mutual_secondproductoutputimaginary ge_balance_negative_mutual_secondproductoutputimaginary. (((((ge_representation_imaginary_code_mutual_secondproductoutput) = 2 * (ge_balance_positive_mutual_secondproductoutputimaginary) /\ (ge_balance_negative_mutual_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_mutual_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_mutual_secondproductoutput) = 2 * ge_signed_half_mutual_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_mutual_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_mutual_secondproductoutputimaginary) = S ge_signed_half_mutual_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_mutual_secondproduct) * (ge_second_ip_mutual_secondproduct))) + (((ge_first_rn_mutual_secondproduct) * (ge_second_in_mutual_secondproduct))))) + (((((ge_first_ip_mutual_secondproduct) * (ge_second_rp_mutual_secondproduct))) + (((ge_first_in_mutual_secondproduct) * (ge_second_rn_mutual_secondproduct))))))) + ge_balance_negative_mutual_secondproductoutputimaginary = (((((((ge_first_rp_mutual_secondproduct) * (ge_second_in_mutual_secondproduct))) + (((ge_first_rn_mutual_secondproduct) * (ge_second_ip_mutual_secondproduct))))) + (((((ge_first_ip_mutual_secondproduct) * (ge_second_rn_mutual_secondproduct))) + (((ge_first_in_mutual_secondproduct) * (ge_second_rp_mutual_secondproduct))))))) + ge_balance_positive_mutual_secondproductoutputimaginary)))))))))) -> (exists gr_unit_mutual_association. ((exists gr_inverse_mutual_associationunit. (exists ge_first_rp_mutual_associationunitidentity ge_first_rn_mutual_associationunitidentity ge_first_ip_mutual_associationunitidentity ge_first_in_mutual_associationunitidentity ge_second_rp_mutual_associationunitidentity ge_second_rn_mutual_associationunitidentity ge_second_ip_mutual_associationunitidentity ge_second_in_mutual_associationunitidentity. ((exists ge_representation_real_code_mutual_associationunitidentityfirst ge_representation_imaginary_code_mutual_associationunitidentityfirst. (((gr_unit_mutual_association) = ((ge_representation_real_code_mutual_associationunitidentityfirst) + (ge_representation_imaginary_code_mutual_associationunitidentityfirst)) * S ((ge_representation_real_code_mutual_associationunitidentityfirst) + (ge_representation_imaginary_code_mutual_associationunitidentityfirst)) + ((ge_representation_imaginary_code_mutual_associationunitidentityfirst) + (ge_representation_imaginary_code_mutual_associationunitidentityfirst))) /\ ((exists ge_balance_positive_mutual_associationunitidentityfirstreal ge_balance_negative_mutual_associationunitidentityfirstreal. (((((ge_representation_real_code_mutual_associationunitidentityfirst) = 2 * (ge_balance_positive_mutual_associationunitidentityfirstreal) /\ (ge_balance_negative_mutual_associationunitidentityfirstreal) = 0) \/ exists ge_signed_half_mutual_associationunitidentityfirstrealdecode. (((ge_representation_real_code_mutual_associationunitidentityfirst) = 2 * ge_signed_half_mutual_associationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_mutual_associationunitidentityfirstreal) = 0) /\ (ge_balance_negative_mutual_associationunitidentityfirstreal) = S ge_signed_half_mutual_associationunitidentityfirstrealdecode))) /\ ((ge_first_rp_mutual_associationunitidentity) + ge_balance_negative_mutual_associationunitidentityfirstreal = (ge_first_rn_mutual_associationunitidentity) + ge_balance_positive_mutual_associationunitidentityfirstreal))) /\ (exists ge_balance_positive_mutual_associationunitidentityfirstimaginary ge_balance_negative_mutual_associationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_mutual_associationunitidentityfirst) = 2 * (ge_balance_positive_mutual_associationunitidentityfirstimaginary) /\ (ge_balance_negative_mutual_associationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_mutual_associationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_mutual_associationunitidentityfirst) = 2 * ge_signed_half_mutual_associationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_mutual_associationunitidentityfirstimaginary) = S ge_signed_half_mutual_associationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_mutual_associationunitidentity) + ge_balance_negative_mutual_associationunitidentityfirstimaginary = (ge_first_in_mutual_associationunitidentity) + ge_balance_positive_mutual_associationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_mutual_associationunitidentitysecond ge_representation_imaginary_code_mutual_associationunitidentitysecond. (((gr_inverse_mutual_associationunit) = ((ge_representation_real_code_mutual_associationunitidentitysecond) + (ge_representation_imaginary_code_mutual_associationunitidentitysecond)) * S ((ge_representation_real_code_mutual_associationunitidentitysecond) + (ge_representation_imaginary_code_mutual_associationunitidentitysecond)) + ((ge_representation_imaginary_code_mutual_associationunitidentitysecond) + (ge_representation_imaginary_code_mutual_associationunitidentitysecond))) /\ ((exists ge_balance_positive_mutual_associationunitidentitysecondreal ge_balance_negative_mutual_associationunitidentitysecondreal. (((((ge_representation_real_code_mutual_associationunitidentitysecond) = 2 * (ge_balance_positive_mutual_associationunitidentitysecondreal) /\ (ge_balance_negative_mutual_associationunitidentitysecondreal) = 0) \/ exists ge_signed_half_mutual_associationunitidentitysecondrealdecode. (((ge_representation_real_code_mutual_associationunitidentitysecond) = 2 * ge_signed_half_mutual_associationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_mutual_associationunitidentitysecondreal) = 0) /\ (ge_balance_negative_mutual_associationunitidentitysecondreal) = S ge_signed_half_mutual_associationunitidentitysecondrealdecode))) /\ ((ge_second_rp_mutual_associationunitidentity) + ge_balance_negative_mutual_associationunitidentitysecondreal = (ge_second_rn_mutual_associationunitidentity) + ge_balance_positive_mutual_associationunitidentitysecondreal))) /\ (exists ge_balance_positive_mutual_associationunitidentitysecondimaginary ge_balance_negative_mutual_associationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_mutual_associationunitidentitysecond) = 2 * (ge_balance_positive_mutual_associationunitidentitysecondimaginary) /\ (ge_balance_negative_mutual_associationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_mutual_associationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_mutual_associationunitidentitysecond) = 2 * ge_signed_half_mutual_associationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_mutual_associationunitidentitysecondimaginary) = S ge_signed_half_mutual_associationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_mutual_associationunitidentity) + ge_balance_negative_mutual_associationunitidentitysecondimaginary = (ge_second_in_mutual_associationunitidentity) + ge_balance_positive_mutual_associationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_mutual_associationunitidentityoutput ge_representation_imaginary_code_mutual_associationunitidentityoutput. (((6) = ((ge_representation_real_code_mutual_associationunitidentityoutput) + (ge_representation_imaginary_code_mutual_associationunitidentityoutput)) * S ((ge_representation_real_code_mutual_associationunitidentityoutput) + (ge_representation_imaginary_code_mutual_associationunitidentityoutput)) + ((ge_representation_imaginary_code_mutual_associationunitidentityoutput) + (ge_representation_imaginary_code_mutual_associationunitidentityoutput))) /\ ((exists ge_balance_positive_mutual_associationunitidentityoutputreal ge_balance_negative_mutual_associationunitidentityoutputreal. (((((ge_representation_real_code_mutual_associationunitidentityoutput) = 2 * (ge_balance_positive_mutual_associationunitidentityoutputreal) /\ (ge_balance_negative_mutual_associationunitidentityoutputreal) = 0) \/ exists ge_signed_half_mutual_associationunitidentityoutputrealdecode. (((ge_representation_real_code_mutual_associationunitidentityoutput) = 2 * ge_signed_half_mutual_associationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_mutual_associationunitidentityoutputreal) = 0) /\ (ge_balance_negative_mutual_associationunitidentityoutputreal) = S ge_signed_half_mutual_associationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_mutual_associationunitidentity) * (ge_second_rp_mutual_associationunitidentity))) + (((ge_first_rn_mutual_associationunitidentity) * (ge_second_rn_mutual_associationunitidentity))))) + (((((ge_first_ip_mutual_associationunitidentity) * (ge_second_in_mutual_associationunitidentity))) + (((ge_first_in_mutual_associationunitidentity) * (ge_second_ip_mutual_associationunitidentity))))))) + ge_balance_negative_mutual_associationunitidentityoutputreal = (((((((ge_first_rp_mutual_associationunitidentity) * (ge_second_rn_mutual_associationunitidentity))) + (((ge_first_rn_mutual_associationunitidentity) * (ge_second_rp_mutual_associationunitidentity))))) + (((((ge_first_ip_mutual_associationunitidentity) * (ge_second_ip_mutual_associationunitidentity))) + (((ge_first_in_mutual_associationunitidentity) * (ge_second_in_mutual_associationunitidentity))))))) + ge_balance_positive_mutual_associationunitidentityoutputreal))) /\ (exists ge_balance_positive_mutual_associationunitidentityoutputimaginary ge_balance_negative_mutual_associationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_mutual_associationunitidentityoutput) = 2 * (ge_balance_positive_mutual_associationunitidentityoutputimaginary) /\ (ge_balance_negative_mutual_associationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_mutual_associationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_mutual_associationunitidentityoutput) = 2 * ge_signed_half_mutual_associationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_mutual_associationunitidentityoutputimaginary) = S ge_signed_half_mutual_associationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_mutual_associationunitidentity) * (ge_second_ip_mutual_associationunitidentity))) + (((ge_first_rn_mutual_associationunitidentity) * (ge_second_in_mutual_associationunitidentity))))) + (((((ge_first_ip_mutual_associationunitidentity) * (ge_second_rp_mutual_associationunitidentity))) + (((ge_first_in_mutual_associationunitidentity) * (ge_second_rn_mutual_associationunitidentity))))))) + ge_balance_negative_mutual_associationunitidentityoutputimaginary = (((((((ge_first_rp_mutual_associationunitidentity) * (ge_second_in_mutual_associationunitidentity))) + (((ge_first_rn_mutual_associationunitidentity) * (ge_second_ip_mutual_associationunitidentity))))) + (((((ge_first_ip_mutual_associationunitidentity) * (ge_second_rn_mutual_associationunitidentity))) + (((ge_first_in_mutual_associationunitidentity) * (ge_second_rp_mutual_associationunitidentity))))))) + ge_balance_positive_mutual_associationunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_mutual_associationtransport ge_first_rn_mutual_associationtransport ge_first_ip_mutual_associationtransport ge_first_in_mutual_associationtransport ge_second_rp_mutual_associationtransport ge_second_rn_mutual_associationtransport ge_second_ip_mutual_associationtransport ge_second_in_mutual_associationtransport. ((exists ge_representation_real_code_mutual_associationtransportfirst ge_representation_imaginary_code_mutual_associationtransportfirst. (((gr_unit_mutual_association) = ((ge_representation_real_code_mutual_associationtransportfirst) + (ge_representation_imaginary_code_mutual_associationtransportfirst)) * S ((ge_representation_real_code_mutual_associationtransportfirst) + (ge_representation_imaginary_code_mutual_associationtransportfirst)) + ((ge_representation_imaginary_code_mutual_associationtransportfirst) + (ge_representation_imaginary_code_mutual_associationtransportfirst))) /\ ((exists ge_balance_positive_mutual_associationtransportfirstreal ge_balance_negative_mutual_associationtransportfirstreal. (((((ge_representation_real_code_mutual_associationtransportfirst) = 2 * (ge_balance_positive_mutual_associationtransportfirstreal) /\ (ge_balance_negative_mutual_associationtransportfirstreal) = 0) \/ exists ge_signed_half_mutual_associationtransportfirstrealdecode. (((ge_representation_real_code_mutual_associationtransportfirst) = 2 * ge_signed_half_mutual_associationtransportfirstrealdecode + 1 /\ (ge_balance_positive_mutual_associationtransportfirstreal) = 0) /\ (ge_balance_negative_mutual_associationtransportfirstreal) = S ge_signed_half_mutual_associationtransportfirstrealdecode))) /\ ((ge_first_rp_mutual_associationtransport) + ge_balance_negative_mutual_associationtransportfirstreal = (ge_first_rn_mutual_associationtransport) + ge_balance_positive_mutual_associationtransportfirstreal))) /\ (exists ge_balance_positive_mutual_associationtransportfirstimaginary ge_balance_negative_mutual_associationtransportfirstimaginary. (((((ge_representation_imaginary_code_mutual_associationtransportfirst) = 2 * (ge_balance_positive_mutual_associationtransportfirstimaginary) /\ (ge_balance_negative_mutual_associationtransportfirstimaginary) = 0) \/ exists ge_signed_half_mutual_associationtransportfirstimaginarydecode. (((ge_representation_imaginary_code_mutual_associationtransportfirst) = 2 * ge_signed_half_mutual_associationtransportfirstimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationtransportfirstimaginary) = 0) /\ (ge_balance_negative_mutual_associationtransportfirstimaginary) = S ge_signed_half_mutual_associationtransportfirstimaginarydecode))) /\ ((ge_first_ip_mutual_associationtransport) + ge_balance_negative_mutual_associationtransportfirstimaginary = (ge_first_in_mutual_associationtransport) + ge_balance_positive_mutual_associationtransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_mutual_associationtransportsecond ge_representation_imaginary_code_mutual_associationtransportsecond. (((a) = ((ge_representation_real_code_mutual_associationtransportsecond) + (ge_representation_imaginary_code_mutual_associationtransportsecond)) * S ((ge_representation_real_code_mutual_associationtransportsecond) + (ge_representation_imaginary_code_mutual_associationtransportsecond)) + ((ge_representation_imaginary_code_mutual_associationtransportsecond) + (ge_representation_imaginary_code_mutual_associationtransportsecond))) /\ ((exists ge_balance_positive_mutual_associationtransportsecondreal ge_balance_negative_mutual_associationtransportsecondreal. (((((ge_representation_real_code_mutual_associationtransportsecond) = 2 * (ge_balance_positive_mutual_associationtransportsecondreal) /\ (ge_balance_negative_mutual_associationtransportsecondreal) = 0) \/ exists ge_signed_half_mutual_associationtransportsecondrealdecode. (((ge_representation_real_code_mutual_associationtransportsecond) = 2 * ge_signed_half_mutual_associationtransportsecondrealdecode + 1 /\ (ge_balance_positive_mutual_associationtransportsecondreal) = 0) /\ (ge_balance_negative_mutual_associationtransportsecondreal) = S ge_signed_half_mutual_associationtransportsecondrealdecode))) /\ ((ge_second_rp_mutual_associationtransport) + ge_balance_negative_mutual_associationtransportsecondreal = (ge_second_rn_mutual_associationtransport) + ge_balance_positive_mutual_associationtransportsecondreal))) /\ (exists ge_balance_positive_mutual_associationtransportsecondimaginary ge_balance_negative_mutual_associationtransportsecondimaginary. (((((ge_representation_imaginary_code_mutual_associationtransportsecond) = 2 * (ge_balance_positive_mutual_associationtransportsecondimaginary) /\ (ge_balance_negative_mutual_associationtransportsecondimaginary) = 0) \/ exists ge_signed_half_mutual_associationtransportsecondimaginarydecode. (((ge_representation_imaginary_code_mutual_associationtransportsecond) = 2 * ge_signed_half_mutual_associationtransportsecondimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationtransportsecondimaginary) = 0) /\ (ge_balance_negative_mutual_associationtransportsecondimaginary) = S ge_signed_half_mutual_associationtransportsecondimaginarydecode))) /\ ((ge_second_ip_mutual_associationtransport) + ge_balance_negative_mutual_associationtransportsecondimaginary = (ge_second_in_mutual_associationtransport) + ge_balance_positive_mutual_associationtransportsecondimaginary)))))) /\ (exists ge_representation_real_code_mutual_associationtransportoutput ge_representation_imaginary_code_mutual_associationtransportoutput. (((b) = ((ge_representation_real_code_mutual_associationtransportoutput) + (ge_representation_imaginary_code_mutual_associationtransportoutput)) * S ((ge_representation_real_code_mutual_associationtransportoutput) + (ge_representation_imaginary_code_mutual_associationtransportoutput)) + ((ge_representation_imaginary_code_mutual_associationtransportoutput) + (ge_representation_imaginary_code_mutual_associationtransportoutput))) /\ ((exists ge_balance_positive_mutual_associationtransportoutputreal ge_balance_negative_mutual_associationtransportoutputreal. (((((ge_representation_real_code_mutual_associationtransportoutput) = 2 * (ge_balance_positive_mutual_associationtransportoutputreal) /\ (ge_balance_negative_mutual_associationtransportoutputreal) = 0) \/ exists ge_signed_half_mutual_associationtransportoutputrealdecode. (((ge_representation_real_code_mutual_associationtransportoutput) = 2 * ge_signed_half_mutual_associationtransportoutputrealdecode + 1 /\ (ge_balance_positive_mutual_associationtransportoutputreal) = 0) /\ (ge_balance_negative_mutual_associationtransportoutputreal) = S ge_signed_half_mutual_associationtransportoutputrealdecode))) /\ ((((((((ge_first_rp_mutual_associationtransport) * (ge_second_rp_mutual_associationtransport))) + (((ge_first_rn_mutual_associationtransport) * (ge_second_rn_mutual_associationtransport))))) + (((((ge_first_ip_mutual_associationtransport) * (ge_second_in_mutual_associationtransport))) + (((ge_first_in_mutual_associationtransport) * (ge_second_ip_mutual_associationtransport))))))) + ge_balance_negative_mutual_associationtransportoutputreal = (((((((ge_first_rp_mutual_associationtransport) * (ge_second_rn_mutual_associationtransport))) + (((ge_first_rn_mutual_associationtransport) * (ge_second_rp_mutual_associationtransport))))) + (((((ge_first_ip_mutual_associationtransport) * (ge_second_ip_mutual_associationtransport))) + (((ge_first_in_mutual_associationtransport) * (ge_second_in_mutual_associationtransport))))))) + ge_balance_positive_mutual_associationtransportoutputreal))) /\ (exists ge_balance_positive_mutual_associationtransportoutputimaginary ge_balance_negative_mutual_associationtransportoutputimaginary. (((((ge_representation_imaginary_code_mutual_associationtransportoutput) = 2 * (ge_balance_positive_mutual_associationtransportoutputimaginary) /\ (ge_balance_negative_mutual_associationtransportoutputimaginary) = 0) \/ exists ge_signed_half_mutual_associationtransportoutputimaginarydecode. (((ge_representation_imaginary_code_mutual_associationtransportoutput) = 2 * ge_signed_half_mutual_associationtransportoutputimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationtransportoutputimaginary) = 0) /\ (ge_balance_negative_mutual_associationtransportoutputimaginary) = S ge_signed_half_mutual_associationtransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_mutual_associationtransport) * (ge_second_ip_mutual_associationtransport))) + (((ge_first_rn_mutual_associationtransport) * (ge_second_in_mutual_associationtransport))))) + (((((ge_first_ip_mutual_associationtransport) * (ge_second_rp_mutual_associationtransport))) + (((ge_first_in_mutual_associationtransport) * (ge_second_rn_mutual_associationtransport))))))) + ge_balance_negative_mutual_associationtransportoutputimaginary = (((((((ge_first_rp_mutual_associationtransport) * (ge_second_in_mutual_associationtransport))) + (((ge_first_rn_mutual_associationtransport) * (ge_second_ip_mutual_associationtransport))))) + (((((ge_first_ip_mutual_associationtransport) * (ge_second_rn_mutual_associationtransport))) + (((ge_first_in_mutual_associationtransport) * (ge_second_rp_mutual_associationtransport))))))) + ge_balance_positive_mutual_associationtransportoutputimaginary)))))))))))

Complete tactic proof in conservative notation

All 80 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

80 script commands · 22 reading checkpoints · 5 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (11)
gaussian zero divides only zerogaussian one unitgaussian multiply one leftgaussian zero validgaussian multiply input right validgaussian multiply associativegaussian multiply cancel leftgaussian multiply one rightgaussian multiply input left validgaussian multiply output transportgaussian multiply commutative
01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hA
  4. L4
    intro hB
02Establish haL5–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eq decidable.

  1. L5
    have ha : a=0 \/ ~(a=0)
  2. L6
    specialize eq_decidable (a)
  3. L7
    specialize eq_decidable (0)
  4. L8
    apply eq_decidable
03Separate the logical casesL9–9

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    cases ha
04Establish hbL10–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian zero divides only zero.

  1. L10
    have hb : b=0
  2. L11
    specialize gaussian_zero_divides_only_zero (b)
  3. L12
    apply gaussian_zero_divides_only_zero
  4. L13
    rewrite ha_left at hA
  5. L14
    exact hA
05Construct an explicit witnessL15–15

Supply the displayed value, then prove that it has the required property.

  1. L15
    exists (6)
06Separate the logical casesL16–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L16
    split
07Use earlier factsL17–17

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L17
    exact gaussian_one_unit
08Calculate and transport equalitiesL18–19

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L18
    rewrite ha_left
  2. L19
    rewrite hb
09Use earlier factsL20–22

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L20
    specialize gaussian_multiply_one_left (0)
  2. L21
    apply gaussian_multiply_one_left
  3. L22
    exact gaussian_zero_valid
10Separate the logical casesL23–24

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L23
    cases hA
  2. L24
    cases hB
11Establish hqL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply exists.

  1. L25
    have hq : ∃ q. GMul(x,x1,q)Definitions: GMul(x,x1,q)Original native command in the exact edition
  2. L26
    specialize gaussian_multiply_exists (x)
  3. L27
    specialize gaussian_multiply_exists (x1)
  4. L28
    apply gaussian_multiply_exists
  5. L29
    specialize gaussian_multiply_input_right_valid (a)
  6. L30
    specialize gaussian_multiply_input_right_valid (x)
  7. L31
    specialize gaussian_multiply_input_right_valid (b)
  8. L32
    apply gaussian_multiply_input_right_valid
  9. L33
    exact hA_witness
  10. L34
    specialize gaussian_multiply_input_right_valid (b)
12Use earlier factsL35–38

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L35
    specialize gaussian_multiply_input_right_valid (x1)
  2. L36
    specialize gaussian_multiply_input_right_valid (a)
  3. L37
    apply gaussian_multiply_input_right_valid
  4. L38
    exact hB_witness
13Separate the logical casesL39–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    cases hq
14Establish hselfL40–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply associative.

  1. L40
    have hself : GMul(a,x2,a)Definitions: GMul(a,x2,a)Original native command in the exact edition
  2. L41
    specialize gaussian_multiply_associative (a)
  3. L42
    specialize gaussian_multiply_associative (x)
  4. L43
    specialize gaussian_multiply_associative (x1)
  5. L44
    specialize gaussian_multiply_associative (b)
  6. L45
    specialize gaussian_multiply_associative (x2)
  7. L46
    specialize gaussian_multiply_associative (a)
  8. L47
    apply gaussian_multiply_associative
  9. L48
    exact hA_witness
  10. L49
    exact hB_witness
15Use earlier factsL50–50

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L50
    exact hq_witness
16Establish heqL51–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply cancel left.

  1. L51
    have heq : x2=6
  2. L52
    specialize gaussian_multiply_cancel_left (a)
  3. L53
    specialize gaussian_multiply_cancel_left (x2)
  4. L54
    specialize gaussian_multiply_cancel_left (6)
  5. L55
    specialize gaussian_multiply_cancel_left (a)
  6. L56
    apply gaussian_multiply_cancel_left
  7. L57
    exact ha_right
  8. L58
    exact hself
  9. L59
    specialize gaussian_multiply_one_right (a)
  10. L60
    apply gaussian_multiply_one_right
17Use earlier factsL61–65

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L61
    specialize gaussian_multiply_input_left_valid (a)
  2. L62
    specialize gaussian_multiply_input_left_valid (x)
  3. L63
    specialize gaussian_multiply_input_left_valid (b)
  4. L64
    apply gaussian_multiply_input_left_valid
  5. L65
    exact hA_witness
18Construct an explicit witnessL66–66

Supply the displayed value, then prove that it has the required property.

  1. L66
    exists (x)
19Separate the logical casesL67–67

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L67
    split
20Construct an explicit witnessL68–68

Supply the displayed value, then prove that it has the required property.

  1. L68
    exists (x1)
21Use earlier factsL69–78

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L69
    specialize gaussian_multiply_output_transport (x)
  2. L70
    specialize gaussian_multiply_output_transport (x1)
  3. L71
    specialize gaussian_multiply_output_transport (x2)
  4. L72
    specialize gaussian_multiply_output_transport (6)
  5. L73
    apply gaussian_multiply_output_transport
  6. L74
    exact heq
  7. L75
    exact hq_witness
  8. L76
    specialize gaussian_multiply_commutative (a)
  9. L77
    specialize gaussian_multiply_commutative (x)
  10. L78
    specialize gaussian_multiply_commutative (b)
22Use earlier factsL79–80

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L79
    apply gaussian_multiply_commutative
  2. L80
    exact hA_witness

Library-wide reading audit

Original defined command ledger · 80 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hA
  4. 0004intro hB
  5. 0005have ha : a=0 \/ ~(a=0)
  6. 0006specialize eq_decidable (a)
  7. 0007specialize eq_decidable (0)
  8. 0008apply eq_decidable
  9. 0009cases ha
  10. 0010have hb : b=0
  11. 0011specialize gaussian_zero_divides_only_zero (b)
  12. 0012apply gaussian_zero_divides_only_zero
  13. 0013rewrite ha_left at hA
  14. 0014exact hA
  15. 0015exists (6)
  16. 0016split
  17. 0017exact gaussian_one_unit
  18. 0018rewrite ha_left
  19. 0019rewrite hb
  20. 0020specialize gaussian_multiply_one_left (0)
  21. 0021apply gaussian_multiply_one_left
  22. 0022exact gaussian_zero_valid
  23. 0023cases hA
  24. 0024cases hB
  25. 0025have hq : ∃ q. GMul(x,x1,q)
  26. 0026specialize gaussian_multiply_exists (x)
  27. 0027specialize gaussian_multiply_exists (x1)
  28. 0028apply gaussian_multiply_exists
  29. 0029specialize gaussian_multiply_input_right_valid (a)
  30. 0030specialize gaussian_multiply_input_right_valid (x)
  31. 0031specialize gaussian_multiply_input_right_valid (b)
  32. 0032apply gaussian_multiply_input_right_valid
  33. 0033exact hA_witness
  34. 0034specialize gaussian_multiply_input_right_valid (b)
  35. 0035specialize gaussian_multiply_input_right_valid (x1)
  36. 0036specialize gaussian_multiply_input_right_valid (a)
  37. 0037apply gaussian_multiply_input_right_valid
  38. 0038exact hB_witness
  39. 0039cases hq
  40. 0040have hself : GMul(a,x2,a)
  41. 0041specialize gaussian_multiply_associative (a)
  42. 0042specialize gaussian_multiply_associative (x)
  43. 0043specialize gaussian_multiply_associative (x1)
  44. 0044specialize gaussian_multiply_associative (b)
  45. 0045specialize gaussian_multiply_associative (x2)
  46. 0046specialize gaussian_multiply_associative (a)
  47. 0047apply gaussian_multiply_associative
  48. 0048exact hA_witness
  49. 0049exact hB_witness
  50. 0050exact hq_witness
  51. 0051have heq : x2=6
  52. 0052specialize gaussian_multiply_cancel_left (a)
  53. 0053specialize gaussian_multiply_cancel_left (x2)
  54. 0054specialize gaussian_multiply_cancel_left (6)
  55. 0055specialize gaussian_multiply_cancel_left (a)
  56. 0056apply gaussian_multiply_cancel_left
  57. 0057exact ha_right
  58. 0058exact hself
  59. 0059specialize gaussian_multiply_one_right (a)
  60. 0060apply gaussian_multiply_one_right
  61. 0061specialize gaussian_multiply_input_left_valid (a)
  62. 0062specialize gaussian_multiply_input_left_valid (x)
  63. 0063specialize gaussian_multiply_input_left_valid (b)
  64. 0064apply gaussian_multiply_input_left_valid
  65. 0065exact hA_witness
  66. 0066exists (x)
  67. 0067split
  68. 0068exists (x1)
  69. 0069specialize gaussian_multiply_output_transport (x)
  70. 0070specialize gaussian_multiply_output_transport (x1)
  71. 0071specialize gaussian_multiply_output_transport (x2)
  72. 0072specialize gaussian_multiply_output_transport (6)
  73. 0073apply gaussian_multiply_output_transport
  74. 0074exact heq
  75. 0075exact hq_witness
  76. 0076specialize gaussian_multiply_commutative (a)
  77. 0077specialize gaussian_multiply_commutative (x)
  78. 0078specialize gaussian_multiply_commutative (b)
  79. 0079apply gaussian_multiply_commutative
  80. 0080exact hA_witness