proposition: Lemma order_div : forall (b : Z) (x p : nat), Order b x p -> forall y : nat, 0 < y -> Mod (Exp b y) 1 p -> Divides x y.
proof: Proof. intros. elim H. intros. elim H3. intros. elim (divdec y x). intro. assumption. intro. elim (notdiv_rem x y H2 H6). intro q. intros. elim H7. intro r. intros. elim H8. intros. elim H10. intros. rewrite H12 in H1. elim (lt_not_le r x). assumption. apply H5. assumption. apply mod_trans with (Exp b (q * x) * Exp b r)%Z. apply mod_trans with (Exp (Exp b x) q * Exp b r)%Z. pattern (Exp b r) at 1 in |- *. replace (Exp b r) with (1 * Exp b r)%Z. apply mod_mult_compat. apply mod_sym. apply mod_exp1. assumption. apply mod_refl. apply Zmult_1_l. rewrite mult_comm. rewrite exp_mult. apply mod_refl. rewrite <- exp_plus. assumption. Qed.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo modprime fermat