proposition: Lemma divdiff_chain (f : Q ->CR) (x y u v: Q): let l:=(x,u):::ne_list.one (y,v) in let sndl:=(ne_list.map snd l) in ¬(u-v == 0)%Q -> (divdiff (ne_list.map (second f ) l)) == (divdiff (ne_zip sndl (ne_list.map f sndl))) * (divdiff (ne_list.map (second inject_Q_CR) l)).
proof: Proof. Proof with auto;simpl. intros. do 3 rewrite divdiff_e... set (s:=f u - f v). set (t:='(/ (x - y))). rewrite CRminus_Qminus. set (a:=(u-v)%Q). transitivity (s * ' (/ (a) * (a))%Q * t). rewrite <- (Qmult_comm a). rewrite Qmult_inv_r... ring. rewrite <- (@CRmult_Qmult (/a) a). set (' (/a)). ring. Qed.
imports: CoRN.model.totalorder.QposMinMax Unicode.Utf8 Setoid Arith List Program Permutation metric2.Classified CSetoids CPoly_ApZero CPoly_Degree CRArith CRArith_alg Qmetric Qring CReals Ranges stdlib_omissions.Pair stdlib_omissions.Q list_separates SetoidPermutation CRings