proposition: Lemma Rlt_sqrt3_0 : 0 < sqrt 3.
proof: Proof. cut (0%nat <> 1%nat); [ intro H0; assert (Hyp : 0 < 2); [ prove_sup0 | generalize (Rlt_le 0 2 Hyp); intro H1; assert (Hyp2 : 0 < 3); [ prove_sup0 | generalize (Rlt_le 0 3 Hyp2); intro H2; generalize (lt_INR_0 1 (proj1 (Nat.neq_0_lt_0 1) (Nat.neq_sym 0 1 H0))); unfold INR; intro H3; generalize (Rplus_lt_compat_l 2 0 1 H3); rewrite Rplus_comm; rewrite Rplus_0_l; replace (2 + 1) with 3; [ intro H4; generalize (sqrt_lt_1 2 3 H1 H2 H4); clear H3; intro H3; apply (Rlt_trans 0 (sqrt 2) (sqrt 3) Rlt_sqrt2_0 H3) | ring ] ] ] | discriminate ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt