proposition: Theorem divisor_smaller : forall m p:nat, 0 < m -> forall q:nat, m = q*p -> q <= m.
proof: Proof. intros m p Hlt; case p. - intros q Heq; rewrite Heq in Hlt; rewrite Nat.mul_comm in Hlt. elim (Nat.lt_irrefl 0);exact Hlt. - intros p' q; case q. + intros Heq; rewrite Heq in Hlt. elim (Nat.lt_irrefl _ Hlt). + intros q' Heq; rewrite Heq. rewrite Nat.mul_comm; simpl; auto with arith. Qed.
imports: ZArith Arith Lia