proposition: Fact Z2Zp_plus 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 ]. + do 3 (rewrite Z2Zp_pos; try lia). rewrite Z2Nat.inj_add; auto. apply nat2Zp_plus. + rewrite Z.add_comm, Zp_add_comm. destruct (Z_pos_or_neg (u+v)). - apply Z2Zp_plus_loc; lia. - apply Z2Zp_plus_loc'; lia. + destruct (Z_pos_or_neg (u+v)). - apply Z2Zp_plus_loc; lia. - apply Z2Zp_plus_loc'; lia. + do 3 (rewrite Z2Zp_neg, Z2Zp_pos; try lia). rewrite <- Zp_opp_plus; f_equal. replace (-(u+v)) with ((-u)+(-v)) by lia. rewrite Z2Nat.inj_add; try lia. apply nat2Zp_plus. 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)