proposition: Theorem div_Zsqrt : forall m n p:Z, 0 < m < n -> n=m*p-> 0 < m <= Z.sqrt n \/ 0 < p <= Z.sqrt n.
proof: Proof. intros m n p Hint Heq. elim (Z_lt_le_dec (Z.sqrt n) m); elim (Z_lt_le_dec (Z.sqrt n) p). - intros Hltm Hltp. assert (Hlem : (Z.sqrt n)+1 <= m) by lia. assert (Hlep : (Z.sqrt n)+1 <= p) by lia. elim (Z.lt_irrefl n). apply Z.lt_le_trans with (((Z.sqrt n)+1)*((Z.sqrt n)+1)). assert (Hposn : 0 <= n) by lia. generalize (Z.sqrt_spec n Hposn);cbv zeta;intro H23. intuition. pattern n at 3; rewrite Heq. apply Zmult_le_compat; try lia. generalize (Z.sqrt_nonneg n). lia. generalize (Z.sqrt_nonneg n). lia. - intros Hple _; right; split; auto. apply Zmult_lt_0_reg_r with m; try tauto. rewrite Zmult_comm; lia. - intros _ Hmle; left; split; tauto. - intros _ Hmle; left; split; tauto. Qed.
imports: ZArith Arith Bool Lia