proposition: Lemma Zmult_reverse : forall x : Z, ~ x %= 0 -> sig (fun y => (x * y) %= 1).
proof: Proof. intros. apply constructive_indefinite_description_Z. intro. unfold "%=", mod_eq. apply Zdivide_dec. cut (Zis_gcd x p 1). intro H0; destruct (Zis_gcd_bezout _ _ _ H0) as [u v H1]. exists u; exists v. rewrite <- H1; ring. constructor; try apply Zone_divide. intros. assert (Z.abs x0<=Z.abs p) by (apply Zdivide_bounds; trivial; destruct p_prime; lia). replace (Z.abs p) with p in H2 by (destruct p; trivial; destruct p_prime; inversion H3). assert(exists x1, 0<=x1<=p /\ (x1 | x) /\ (x1 | p) /\ Z.abs x0 = x1). destruct x0. now destruct H1; ring_simplify in H1; destruct p_prime; clear H; subst; inversion H3. exists (Zpos p0); repeat split; auto; apply Zle_0_pos. exists (-Zneg p0); repeat split; try rewrite Zopp_neg; auto with *. clear H0 H1 H2. destruct H3; destruct H0; destruct H1; destruct H0; destruct H2. cut (x1 | 1). intro; destruct x0; simpl in H4; try (subst; assumption). apply Zdivide_opp_l_rev; rewrite Zopp_neg; rewrite H4; assumption. destruct (dec_Zle x1 1). apply Zle_lt_or_eq in H0. destruct H0. replace x1 with 1 by (apply Zlt_le_succ in H0; simpl in H0; apply Zle_antisym; assumption). apply Zone_divide. rewrite <- H0 in H2; destruct H2; ring_simplify in H2. destruct p_prime; rewrite H2 in H6; inversion H6. apply Znot_le_gt in H5. destruct (dec_Zlt x1 p). destruct p_prime. apply (H8 x1). split; lia. apply Z.divide_refl. assumption. apply False_ind; apply H. ring_simplify. apply Zdivide_opp_r. replace p with x1 by (apply Zle_antisym; lia). assumption. Qed.
imports: Arith ZArith RelationClasses Type_class_definition Lia ZArith Znumtheory ZArith Znumtheory ConstructiveEpsilon