proposition: Theorem sqrt_mibq : forall a b : R, forall ai bi zi : FF, BND a ai -> BND b bi -> BND (sqrt (1 + (a - b) / b) - 1) zi -> Fpos0 (lower ai) && Fpos (lower bi) = true -> BND ((sqrt a - sqrt b) / sqrt b) zi.
proof: Proof. intros a b ai bi zi Ha Hb Hz H. generalize (andb_prop _ _ H). clear H. intros (H1,H2). generalize (Fpos0_correct _ H1). clear H1. intro H1. generalize (Fpos_correct _ H2). clear H2. intro H2. replace ((sqrt a - sqrt b) / sqrt b)%R with (sqrt (1 + (a - b) / b) - 1)%R. exact Hz. replace (1 + (a - b) / b)%R with (a / b)%R. rewrite sqrt_div. field. apply Rgt_not_eq. unfold Rgt. apply sqrt_lt_R0. apply Rlt_le_trans with (1 := H2) (2 := proj1 Hb). apply Rle_trans with (1 := H1) (2 := proj1 Ha). apply Rlt_le_trans with (1 := H2) (2 := proj1 Hb). field. apply Rgt_not_eq. unfold Rgt. apply Rlt_le_trans with (1 := H2) (2 := proj1 Hb). Qed.
imports: Reals Gappa_common