proposition: Lemma Rlt_sqrt2_0 : 0 < sqrt 2.
proof: Proof. assert (Hyp : 0 < 2); [ prove_sup0 | generalize (sqrt_positivity 2 (Rlt_le 0 2 Hyp)); intro H1; elim H1; intro H2; [ assumption | absurd (0 = sqrt 2); [ apply (not_eq_sym (A:=R)); apply sqrt2_neq_0 | assumption ] ] ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt