proposition: Lemma sqrt2_lower_bound ih il j: Φ (WW ih il) < (φ j + 1) ^ 2 -> φ ih <= φ j.
proof: Proof. intros H1. case (to_Z_bounded j); intros Hbj _. case (to_Z_bounded il); intros Hbil _. case (to_Z_bounded ih); intros Hbih Hbih1. assert ((φ ih < φ j + 1)%Z); auto with zarith. apply Zlt_square_simpl; auto with zarith. simpl zn2z_to_Z in H1. repeat rewrite <-Z.pow_2_r. refine (Z.le_lt_trans _ _ _ _ H1). apply Z.le_trans with (φ ih * wB)%Z;try rewrite Z.pow_2_r; auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63