proposition: Lemma XminMultPosDistribOne : forall {R : ConstructiveReals} {X : Set} (f : PartialFunction X) (a : CRcarrier R) (aPos : 0 < a), PartialFunExtEq (Xscale a (XminConst (Xscale (CRinv _ a (inr aPos)) f) 1)) (XminConst f a).
proof: Proof. intros. split. split. - intros x xD. destruct f; exact xD. - intros x xD. destruct f; exact xD. - intros. rewrite applyXscale. simpl in xD, xG. rewrite applyXminConst. rewrite applyXminConst. rewrite applyXscale. rewrite (DomainProp _ _ xD xG). rewrite <- CRmin_mult. rewrite <- CRmult_assoc, CRinv_r, CRmult_1_l. rewrite CRmult_1_r. reflexivity. apply CRlt_asym, aPos. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete