proposition: Lemma DoneMinusX2 : Derivative (clcr (inj_Q IR (-(1))) (inj_Q IR (1:Q))) (inj_Q_less _ (-1) 1 eq_refl) ([-C-]([1]:IR){-}(Two:IR){**}FId{^}2) ([-C-]([0]:IR){-}(Two:IR){**}((nring 2){**}([-C-][1]{*}FId{^}1))).
proof: Proof. apply Derivative_minus. apply Derivative_const. apply Derivative_scal. apply Derivative_nth. apply Derivative_id. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.reals.fast.CRsin CoRN.reals.fast.CRpi CoRN.reals.fast.CRIR CoRN.reals.fast.Compress Coq.QArith.Qpower CoRN.model.ordfields.Qordfield Coq.QArith.Qround CoRN.transc.Pi CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.transc.SinCos CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra