proposition: Fact Z2Zp_mult u v : 〘u*v〙=〘u〙⊗〘v〙.
proof: Proof. destruct (Z_pos_or_neg u) as [ H1 | H1 ]; destruct (Z_pos_or_neg v) as [ H2 | H2 ]. + apply Z2Zp_mult_loc; auto. + replace (u*v) with (-(u*-v)); try ring. rewrite Z2Zp_opp, Z2Zp_mult_loc; try lia. rewrite Z2Zp_opp, Zp_mul_comm, Zp_opp_mult, Zp_opp_inv. apply Zp_mul_comm. + replace (u*v) with (- ((-u)*v)); try ring. rewrite Z2Zp_opp, Z2Zp_mult_loc; try lia. rewrite Z2Zp_opp, Zp_opp_mult, Zp_opp_inv; auto. + replace (u*v) with ((-u)*(-v)); try ring. rewrite Z2Zp_mult_loc; try lia. do 2 rewrite Z2Zp_opp. do 2 rewrite Zp_opp_mult, Zp_mul_comm. apply Zp_opp_inv. Qed.
imports: Arith Lia ZArith List Permutation Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime binomial sums php) Undecidability.H10.ArithLibs(matrix)