proposition: Lemma XminMultPosDistrib : forall {X : Set} {R : ConstructiveReals} (f : PartialFunction X) (a b : CRcarrier R), 0 <= a -> PartialFunExtEq (Xscale a (XminConst f b)) (XminConst (Xscale a f) (a*b)).
proof: Proof. intros. destruct f; simpl; split; unfold DomainInclusion, Domain. - split. + intros x xdf. exact xdf. + intros x xdf. exact xdf. - intros x xdf xg. simpl. rewrite CRmin_mult. rewrite (DomainProp0 x xdf xg). reflexivity. exact H. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete