proposition: Lemma sqrt3_2_neq_0 : 2 * sqrt 3 <> 0.
proof: Proof. apply prod_neq_R0; [ discrR | assert (Hyp : 0 < 3); [ prove_sup0 | generalize (Rlt_le 0 3 Hyp); intro H1; red; intro H2; generalize (sqrt_eq_0 3 H1 H2); intro H; absurd (3 = 0); [ discrR | assumption ] ] ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt