proposition: Lemma unary_diff_correct : forall o f d x, Xderive_pt f x d -> let v := unary (diff_operations _ ext_operations) o (f x, d) in unary ext_operations o (f x) = fst v /\ Xderive_pt (fun x0 => unary ext_operations o (f x0)) x (snd v).
proof: Proof. intros o f d x Hd. destruct o ; simpl ; repeat split. now apply Xderive_pt_neg. now apply Xderive_pt_abs. rewrite rewrite_inv_diff. now apply Xderive_pt_inv. eapply Xderive_pt_eq_fun. 2: now apply Xderive_pt_mul. intros y. simpl. now case f. now apply Xderive_pt_sqrt. now apply Xderive_pt_cos. now apply Xderive_pt_sin. now apply Xderive_pt_tan. now apply Xderive_pt_atan. now apply Xderive_pt_exp. now apply Xderive_pt_ln. now apply Xderive_pt_power_int. now destruct x. now destruct x. now destruct x. now destruct x. now destruct x. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog