proposition: Lemma Rsqrt_positivity : forall x:nonnegreal, 0 <= Rsqrt x.
proof: Proof. intro. destruct (Rsqrt_exists (nonneg x) (cond_nonneg x)) as (x0 & H1 & H2). cut (x0 = Rsqrt x). - intros. rewrite <- H; assumption. - unfold Rsqrt. case (Rsqrt_exists x (cond_nonneg x)) as (?,[]). apply Rsqr_inj. + assumption. + assumption. + rewrite <- H0, <- H2; reflexivity. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra