proposition: Lemma XmultiTriangleIneg : forall {X : Set} {R : ConstructiveReals} (fn : nat -> @PartialFunction R X) (n : nat) (x : X) (xD : Domain (Xabs (Xsum fn n)) x) (y : Domain (Xsum (fun a : nat => Xabs (fn a)) n) x), partialApply (Xabs (Xsum fn n)) x xD <= partialApply (Xsum (fun a : nat => Xabs (fn a)) n) x y.
proof: Proof. induction n. - intros. simpl. simpl in xD. rewrite (DomainProp _ _ xD y). apply CRle_refl. - intros. simpl. simpl in x,y,xD. destruct (Xsum fn n), (fn (S n)), (Xsum (fun a : nat => Xabs (fn a)) n), xD, y; simpl; simpl in IHn. apply (CRle_trans _ (CRabs _ (partialApply0 x d) + CRabs _ (partialApply1 x d0))). apply CRabs_triang. apply CRplus_le_compat. apply IHn. rewrite (DomainProp1 x d0 d2). apply CRle_refl. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete