proposition: Fact Zp_mult_one : forall x, Op ⊗ x = x.
proof: Proof. intros (x & ?); apply Zp_inj; simpl proj1_sig. destruct p as [ | [ | q ] ]. + destruct Hp; auto. + rewrite rem_diag; simpl; auto. rewrite rem_lt; lia. + rewrite rem_lt with (a := 1); try lia. rewrite Nat.mul_1_l, rem_lt; lia. 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)