proposition: Lemma order_le_predp : forall (b : Z) (q p : nat), Prime p -> Order b q p -> q <= pred p.
proof: Proof. intros. elim H. intros. elim H0. intros. elim H4. intros. apply H6. apply lt_pred. assumption. apply flt. assumption. intro. elim (mod_0not1 p). assumption. apply mod_trans with (Exp b q). apply mod_sym. apply moda0_exp_compat. unfold gt in |- *. unfold gt in H1. unfold lt in |- *. apply lt_le_weak. assumption. assumption. assumption. assumption. Qed.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo modprime fermat