proposition: Lemma sqrbound : forall p q : nat, p * p <= p * q \/ q * q <= p * q.
proof: Proof. intros. elim (le_or_lt p q). left. apply le_mult_l. assumption. right. apply le_mult_r. apply lt_le_weak. assumption. Qed.
imports: ZArith EqNat