proposition: Lemma tan_PI4 : tan (PI / 4) = 1.
proof: Proof. unfold tan; rewrite sin_cos_PI4. unfold Rdiv; apply Rinv_r. change (cos (PI / 4) <> 0); rewrite cos_PI4; apply R1_sqrt2_neq_0. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt