proposition: Lemma toRad_inj : forall x y:R, toRad x = toRad y -> x = y.
proof: Proof. intros; unfold toRad in H; apply Rmult_eq_reg_l with PI. - rewrite <- (Rmult_comm x); rewrite <- (Rmult_comm y). apply Rmult_eq_reg_l with (/ plat). + rewrite <- (Rmult_comm (x * PI)); rewrite <- (Rmult_comm (y * PI)); assumption. + apply Rinv_neq_0_compat; unfold plat; discrR. - apply PI_neq0. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt