proposition: Theorem Zp_mult_autoinv l : ~ list_has_dup l -> (forall x, In x l -> x <> Zp /\ inv x <> x /\ In (inv x) l) -> Zp_lprod l = Op.
proof: Proof. induction on l as IHl with measure (length l); intros H0 Hl. destruct l as [ | x l ]. + rewrite Zp_lprod_nil; auto. + destruct (Hl x) as (H1 & H2 & [H3 | H3]); try (simpl; auto; fail). 1: destruct H2; auto. destruct in_split with (1 := H3) as (u & v & ?); subst. rewrite Zp_lprod_cons, Zp_lprod_app, Zp_lprod_cons. rewrite (Zp_mul_assoc _ (inv x)), (Zp_mul_comm _ (inv x)). repeat rewrite Zp_mul_assoc. rewrite (Zp_mul_comm _ (inv x)), Zp_invert_spec2; auto. rewrite Zp_mult_one, <- Zp_lprod_app. apply IHl. * simpl; do 2 rewrite app_length; simpl; lia. * contradict H0. constructor 2. apply perm_list_has_dup with (inv x::u++v). - apply Permutation_cons_app; auto. - constructor 2; auto. * intros y Hy. destruct (Hl y) as (G1 & G2 & G3). - apply in_app_or in Hy; right; apply in_or_app; simpl; tauto. - repeat (split; auto). destruct G3 as [ G3 | G3 ]. ++ destruct H0; rewrite G3 at 2. rewrite Zp_invert_involutive. constructor 2. apply perm_list_has_dup with (y::u++v). ** apply Permutation_cons_app; auto. ** constructor 1; auto. ++ apply in_or_app. apply in_app_or in G3. destruct G3 as [ | [ G3 | ] ]; try tauto. exfalso. apply f_equal with (f := inv) in G3. do 2 rewrite Zp_invert_involutive in G3. destruct H0. apply perm_list_has_dup with (inv x::(x::u)++v). ** apply Permutation_cons_app with (l1 := x::u); auto. ** simpl; constructor 2; constructor 1; subst; auto. 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)