proposition: Theorem sqrtG: forall x : R, forall xi zi : FF, BND x xi -> sqrt_helper xi zi = true -> BND (sqrt x) zi.
proof: Proof. intros x xi zi Hx Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fpos0_correct _ H2). clear H2. intro H2. generalize (Fle2_correct _ _ H3). rewrite Fmult2_correct. clear H3. intro H3. unfold BND. apply IRsqrt with (2 := H2) (3 := H3) (4 := Hx). induction (lower zi). induction Fnum ; simpl in H1. rewrite float2_zero. rewrite Rmult_0_l. assert (H4 := Fpos0_correct _ H1). case (Rlt_le_dec 0 0) ; intros _ ; exact H4. case (Rlt_le_dec 0 (Float2 (Zpos p) Fexp)). intros _. rewrite <- Fmult2_correct. apply Fle2_correct. exact H1. intro H. elim (Rlt_irrefl R0). apply Rlt_le_trans with (2 := H). apply Fpos_correct. apply refl_equal. case (Rlt_le_dec 0 (Float2 (Zneg p) Fexp)). intro H. elim (Rlt_irrefl R0). apply Rlt_trans with (1 := H). apply Fneg_correct. apply refl_equal. intros _. apply Fpos0_correct. exact H1. Qed.
imports: Gappa_common Gappa_decimal