proposition: Fact Zp_mult_revert : forall x i, i ⊗ x = Op -> is_gcd p (proj1_sig x) 1.
proof: Proof. intros (x & Hx) (i & Hi) H; simpl. apply f_equal with (f := @proj1_sig _ _) in H; simpl in H. destruct (le_lt_dec p 1) as [ H' | H']. + replace p with 1 by lia. apply is_gcd_1l. + rewrite rem_lt with (a := 1) in H; try lia. generalize (div_rem_spec1 (i*x) p). rewrite H. generalize (div (i*x) p); clear H Hi; intros u Hu. apply bezout_sc with 1 i ((1+u)* p). * rewrite Hu; ring. * left; apply divides_mult, divides_refl. 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)