proposition: Lemma mod_repr_eq : forall (p : nat) (x y : Z), 0 < p -> (0 < x < Z_of_nat p)%Z -> (0 < y < Z_of_nat p)%Z -> Mod x y p -> x = y.
proof: Proof. intros. unfold Mod in H2. elim H2. intros q Hq. rewrite Hq in H0. elim H0. elim H1. intros. elim (Zle_or_lt 0 q). intro. elim (Zle_lt_or_eq 0 q). intro. elim (Zlt_not_le 0 y). assumption. apply Zplus_le_reg_l with (Z_of_nat p). rewrite (Zplus_comm (Z_of_nat p)). rewrite (Zplus_comm (Z_of_nat p)). simpl in |- *. apply Zlt_le_weak. apply Z.le_lt_trans with (y + Z_of_nat p * q)%Z. apply Zplus_le_compat_l. pattern (Z_of_nat p) at 1 in |- *. rewrite <- Zmult_1_l with (Z_of_nat p). rewrite (Zmult_comm 1). apply Zle_mult_l. change (Z_of_nat 0 < Z_of_nat p)%Z in |- *. apply Znat.inj_lt. assumption. change (Z.succ 0 <= q)%Z in |- *. apply Zlt_le_succ. assumption. assumption. intro. rewrite <- H8 in Hq. rewrite Zmult_comm in Hq. rewrite Zplus_comm in Hq. simpl in Hq. assumption. assumption. intro. elim (Zlt_not_le 0 (y + Z_of_nat p * q)). assumption. apply Z.le_trans with (y + Z_of_nat p * -1)%Z. apply Zplus_le_compat_l. apply Zle_mult_l. change (Z_of_nat 0 < Z_of_nat p)%Z in |- *. apply Znat.inj_lt. assumption. apply Zlt_succ_le. simpl in |- *. assumption. apply Zplus_le_reg_l with (Z_of_nat p). rewrite (Zplus_comm (Z_of_nat p)). rewrite (Zplus_comm (Z_of_nat p)). rewrite (Zmult_comm (Z_of_nat p)). rewrite (Zopp_mult_distr_l_reverse 1). rewrite Zmult_1_l. rewrite Zplus_assoc_reverse. rewrite Zplus_opp_l. rewrite (Zplus_comm y 0). simpl in |- *. apply Zlt_le_weak. assumption. Qed.
imports: ZArith lemmas natZ exp divides