proposition: Lemma XscaleAssoc : forall {R : ConstructiveReals} {X : Set} (f : PartialFunction X) (a b : CRcarrier R), PartialFunExtEq (Xscale a (Xscale b f)) (Xscale (a*b) f).
proof: Proof. intros. destruct f; simpl; split. - split. + intros x. simpl. exact (fun x => x). + intros x. simpl. exact (fun x => x). - intros. simpl. rewrite (DomainProp0 x xD xG). rewrite CRmult_assoc. reflexivity. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete