proposition: Lemma binary_diff_correct : forall o f1 f2 d1 d2 x, Xderive_pt f1 x d1 -> Xderive_pt f2 x d2 -> let v := binary (diff_operations _ ext_operations) o (f1 x, d1) (f2 x, d2) in binary ext_operations o (f1 x) (f2 x) = fst v /\ Xderive_pt (fun x0 => binary ext_operations o (f1 x0) (f2 x0)) x (snd v).
proof: Proof. intros o f1 f2 d1 d2 x Hd1 Hd2. destruct o ; simpl ; repeat split. now apply Xderive_pt_add. now apply Xderive_pt_sub. now apply Xderive_pt_mul. rewrite rewrite_div_diff. now apply Xderive_pt_div. 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