proposition: Lemma XscaleOne : forall {X : Set} {R : ConstructiveReals} (f : @PartialFunction R X), PartialFunExtEq (Xscale 1 f) f.
proof: Proof. intros. split. - split. + intros x H. destruct f; exact H. + intros x H. destruct f; exact H. - intros. rewrite applyXscale, CRmult_1_l. apply DomainProp. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete