proposition: Theorem sqrt_xibu : forall a : R, forall ai zi : FF, BND a ai -> BND (sqrt a * sqrt a) zi -> Fpos0 (lower ai) = true -> BND a zi.
proof: Proof. intros a ai zi Ha Hz H. generalize (Fpos0_correct _ H). clear H. intro H. rewrite <- (sqrt_sqrt a). exact Hz. apply Rle_trans with (1 := H). apply Ha. Qed.
imports: Reals Gappa_common