proposition: Lemma binary_diff_bnd_correct : forall prec o f1 f2 f1' f2', let u x := binary (diff_operations _ ext_operations) o (f1 x, f1' x) (f2 x, f2' x) in forall yi1 yi2 yi1' yi2' xi, (forall x, contains xi x -> contains (I.convert yi1) (f1 x)) -> (forall x, contains xi x -> contains (I.convert yi2) (f2 x)) -> (forall x, contains xi x -> contains (I.convert yi1') (f1' x)) -> (forall x, contains xi x -> contains (I.convert yi2') (f2' x)) -> let v := binary (diff_operations _ (BndValuator.operations prec)) o (yi1, yi1') (yi2, yi2') in (forall x, contains xi x -> contains (I.convert (snd v)) (snd (u x))).
proof: Proof. intros prec o f1 f2 f1' f2' u yi1 yi2 yi1' yi2' xi Hf1 Hf2 Hf1' Hf2' v x Hx. destruct o ; simpl ; repeat first [ apply I.add_correct | apply I.sub_correct | apply I.mul_correct | apply I.div_correct ] ; now first [ apply Hf1 | apply Hf2 | apply Hf1' | apply Hf2' ]. 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