proposition: Lemma div_le1 : forall n d : nat, Divides d (S n) -> d <= S n.
proof: Proof. unfold Divides in |- *. intros. elim H. intro q. case q. rewrite <- (mult_n_O d). intros. discriminate H0. intro q1. intros. rewrite H0. apply le_n_nm. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp