proposition: Lemma sqrt_test_false i j: 0 <= i -> 0 < j -> i/j < j -> (j + (i/j))/2 < j.
proof: Proof. intros Hi Hj; elim_div; intros q r [ ? hr ]; [ lia | subst i ]. elim_div; intros a b [ h [ hb | ] ]; lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63