proposition: Lemma dd_indep : forall (l1 l2 : seq K) (P1 : fresh_seq K l1) (P2 : fresh_seq K l2), l1 = l2 -> dd K f l1 P1 [=] dd K f l2 P2.
proof: Proof. intros. unfold dd. replace (existT (fun s : seq K => fresh_seq K s) l2 P2) with (existT (fun s : seq K => fresh_seq K s) l1 P1). reflexivity. by apply subsetT_eq_compat. Qed.
imports: ssreflect CSetoids CSetoidFun CFields CPolynomials Program Omega Equivalence Morphisms Wf Morphisms CRings CRing_Homomorphisms Rational Setoid CPoly_NthCoeff CPoly_Degree CReals Intervals CauchySeq IntervalFunct MoreIntervals MoreFunctions Composition seq bigopsClass