proposition: Lemma rewrite_inv_diff : forall u u', Xmul u' (Xneg (Xsqr (Xinv u))) = Xneg (Xdiv u' (Xsqr u)).
proof: Proof. intros. rewrite Xmul_Xneg_distr_r. apply f_equal. rewrite Xdiv_split. apply f_equal. assert (forall x, Xsqr x = Xmul x x) by now intros [|x]. rewrite 2!H. apply sym_eq. apply Xinv_Xmul_distr. 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