proposition: Lemma rewrite_div_diff : forall u v u' v', Xdiv (Xsub u' (Xmul v' (Xdiv u v))) v = Xdiv (Xsub (Xmul u' v) (Xmul v' u)) (Xmul v v).
proof: Proof. intros. repeat rewrite Xdiv_split. rewrite Xinv_Xmul_distr. repeat rewrite <- Xmul_assoc. apply (f_equal (fun x => Xmul x (Xinv v))). rewrite 2!Xsub_split. rewrite Xadd_comm. set (w := Xmul v' u). rewrite Xmul_Xadd_distr_r. rewrite Xmul_assoc Xmul_Xinv. destruct (Xinv v) as [|z]. by rewrite /= 2!Xlift2_nan_r. rewrite /= Xmul_1_r Xmul_Xneg_distr_l. apply Xadd_comm. 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