proposition: Theorem sqrt_mibs : forall a b : R, forall ai bi zi : FF, BND a ai -> BND b bi -> BND ((a - b) / (sqrt a + sqrt b)) zi -> Fpos0 (lower ai) && Fpos0 (lower bi) = true -> BND (sqrt a - 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 (Fpos0_correct _ H2). clear H2. intro H2. assert (H3: (0 <= sqrt a)%R). apply sqrt_positivity. apply Rle_trans with (1 := H1) (2 := proj1 Ha). assert (H4: (0 <= sqrt b)%R). apply sqrt_positivity. apply Rle_trans with (1 := H2) (2 := proj1 Hb). case (Rtotal_order (sqrt a + sqrt b) 0). intro H. elim Rlt_not_le with (1 := H). apply Rplus_le_le_0_compat ; assumption. intros [H|H] ; replace (sqrt a - sqrt b)%R with ((a - b) / (sqrt a + sqrt b))%R ; try exact Hz. assert (sqrt a = 0)%R. apply Rle_antisym. 2: exact H3. rewrite <- H. pattern (sqrt a) at 1 ; rewrite <- (Rplus_0_r (sqrt a)). apply Rplus_le_compat_l with (1 := H4). rewrite H0 in H. rewrite Rplus_0_l in H. rewrite H. rewrite H0. assert (a = 0)%R as ->. apply sqrt_eq_0 with (2 := H0). apply Rle_trans with (1 := H1) (2 := proj1 Ha). assert (b = 0)%R as ->. apply sqrt_eq_0 with (2 := H). apply Rle_trans with (1 := H2) (2 := proj1 Hb). rewrite Rminus_0_r. unfold Rdiv. apply Rmult_0_l. replace (a - b)%R with (sqrt a * sqrt a - sqrt b * sqrt b)%R. field. now apply Rgt_not_eq. repeat rewrite sqrt_def. exact (refl_equal _). apply Rle_trans with (1 := H2) (2 := proj1 Hb). apply Rle_trans with (1 := H1) (2 := proj1 Ha). Qed.
imports: Reals Gappa_common