proposition: Lemma R1_sqrt2_neq_0 : 1 / sqrt 2 <> 0.
proof: Proof. generalize (Rinv_neq_0_compat (sqrt 2) sqrt2_neq_0); intro H; generalize (prod_neq_R0 1 (/ sqrt 2) R1_neq_R0 H); intro H0; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt