proposition: Lemma formule : forall (x h l1 l2:R) (f1 f2:R -> R), h <> 0 -> f2 x <> 0 -> f2 (x + h) <> 0 -> (f1 (x + h) / f2 (x + h) - f1 x / f2 x) / h - (l1 * f2 x - l2 * f1 x) / Rsqr (f2 x) = / f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1) + l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h)) - f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2) + l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x).
proof: Proof. intros; unfold Rdiv, Rminus, Rsqr. repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l; repeat rewrite Rinv_mult. replace (l1 * f2 x * (/ f2 x * / f2 x)) with (l1 * / f2 x * (f2 x * / f2 x)); [ idtac | ring ]. replace (l1 * (/ f2 x * / f2 (x + h)) * f2 x) with (l1 * / f2 (x + h) * (f2 x * / f2 x)); [ idtac | ring ]. replace (l1 * (/ f2 x * / f2 (x + h)) * - f2 (x + h)) with (- (l1 * / f2 x * (f2 (x + h) * / f2 (x + h)))); [ idtac | ring ]. replace (f1 x * (/ f2 x * / f2 (x + h)) * (f2 (x + h) * / h)) with (f1 x * / f2 x * / h * (f2 (x + h) * / f2 (x + h))); [ idtac | ring ]. replace (f1 x * (/ f2 x * / f2 (x + h)) * (- f2 x * / h)) with (- (f1 x * / f2 (x + h) * / h * (f2 x * / f2 x))); [ idtac | ring ]. replace (l2 * f1 x * (/ f2 x * / f2 x * / f2 (x + h)) * f2 (x + h)) with (l2 * f1 x * / f2 x * / f2 x * (f2 (x + h) * / f2 (x + h))); [ idtac | ring ]. replace (l2 * f1 x * (/ f2 x * / f2 x * / f2 (x + h)) * - f2 x) with (- (l2 * f1 x * / f2 x * / f2 (x + h) * (f2 x * / f2 x))); [ idtac | ring ]. repeat rewrite Rinv_r; try assumption || ring. Qed.
imports: Rbase Rfunctions Ranalysis1 Lra