proposition: Lemma sqrt_no_R0 : forall z : R, 0 < z -> sqrt z <> 0.
proof: Proof. intros z z_pos Hf ; destruct (Rlt_irrefl 0) ; eapply Rlt_le_trans ; [| right ; eapply sqrt_eq_0 ; [left |]] ; eassumption. Qed.
imports: Rbase AltSeries Rseries_def Rtrigo_facts Ratan Cpow_plus Complex Lra MyRIneq