proposition: Theorem sqrdivbound : forall n d : nat, Divides d n -> exists x : nat, Divides x n /\ x * x <= n /\ (x = d \/ d * x = n).
proof: Proof. intros. unfold Divides in H. elim H. intros. rewrite H0. elim (sqrbound d x). intros. split with d. split. split with x. reflexivity. split. assumption. left. reflexivity. intros. split with x. split. split with d. apply mult_comm. split. assumption. right. reflexivity. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp