proposition: Lemma div_le : forall d n : nat, 0 < n -> Divides d n -> d <= n.
proof: Proof. intros d n. case n. intro. elim (lt_irrefl 0). assumption. intros. apply div_le1. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp