proposition: Lemma StepFSupBallBind(X:MetricSpace): ((forall (e : Qpos) (a b : StepF (StepFS (msp_as_RSetoid X))) , forall f:(StepFS (msp_as_RSetoid X)) -->(StepFS (msp_as_RSetoid X)), (forall c d, (StepFSupBall (proj1_sig e) c d) -> (StepFSupBall (proj1_sig e) (f c) (f d)))-> StepFSupBall (X:=StepFSup X) (proj1_sig e) a b -> StepFSupBall (X:=X) (proj1_sig e) (StFBind00 a f) (StFBind00 b f))).
proof: Proof. intros e a. unfold ball_ex. induction a. simpl. induction b. intros. simpl. apply H. assumption. intros f Hf H. simpl in H. unfold StepFSupBall in H. pose proof (GlueAp (constStepF (ballS (StepFSup X) (proj1_sig e)) <@^ x) o b1 b2). rewrite H0 in H. clear H0. rewrite -> StepFfoldPropglue_rew in H. destruct H as [H H1]. simpl. unfold StepFSupBall. rewrite -> GlueAp. rewrite -> StepFfoldPropglue_rew. split. pose (HH:=IHb1 (compose1 (SplitLS (msp_as_RSetoid X) o) f)). simpl in HH. simpl in HH. unfold StepFSupBall in HH. unfold compose0 in HH. assert (rew:(ballS X (proj1_sig e) ^@> SplitLS0 o (f x)) == (SplitL (ballS X (proj1_sig e) ^@> f x) o)). unfold SplitLS0. rewrite SplitLMap;reflexivity. rewrite <-rew. clear rew. apply HH; auto with *. intros. unfold SplitLS0. rewrite <- SplitLMap. rewrite <- SplitLAp. apply StepFfoldPropSplitL. apply (Hf c d H0). pose (HH:=IHb2 (compose1 (SplitRS (msp_as_RSetoid X) o) f)). simpl in HH. unfold StepFSupBall in HH. unfold compose0 in HH. assert (rew:(ballS X (proj1_sig e) ^@> SplitRS0 o (f x)) == (SplitR (ballS X (proj1_sig e) ^@> f x) o)). unfold SplitRS0. rewrite SplitRMap;reflexivity. rewrite <-rew. clear rew. apply HH; auto with *. intros. unfold SplitRS0. rewrite <- SplitRMap. rewrite <- SplitRAp. apply StepFfoldPropSplitR. apply (Hf c d H0). intros b f Hf H. simpl. unfold StepFSupBall. simpl. rewrite MapGlue. rewrite ApGlue. rewrite -> StepFfoldPropglue_rew. split. clear IHa2. pose (HH:=IHa1 (SplitL b o) (compose1 (SplitLS (msp_as_RSetoid X) o) f)). simpl in HH. unfold compose0 in HH. unfold StepFSupBall in HH. rewrite -> SplitLBind. apply HH; clear HH. intros. unfold SplitLS0. rewrite <- SplitLMap. rewrite <- SplitLAp. apply StepFfoldPropSplitL. apply (Hf c d H0). pose (HH:=StepFfoldPropSplitL _ o H). rewrite -> SplitLAp in HH. rewrite SplitLMap in HH. assert (StepF_eq (ballS (StepFSup X) (proj1_sig e) ^@> a1 <@> SplitL b o) (ballS (StepFSup X) (proj1_sig e) ^@> SplitL (glue o a1 a2) o <@> SplitL b o)). { rewrite SplitLGlue. reflexivity. } rewrite (StepFfoldProp_mor _ _ H0). exact HH. clear IHa1. pose (HH:=IHa2 (SplitR b o) (compose1 (SplitRS (msp_as_RSetoid X) o) f)). simpl in HH. unfold compose0 in HH. unfold StepFSupBall in HH. rewrite -> SplitRBind. apply HH; clear HH. intros. unfold SplitRS0. rewrite <- SplitRMap. rewrite <- SplitRAp. apply StepFfoldPropSplitR. apply (Hf c d H0). pose (HH:=StepFfoldPropSplitR _ o H). rewrite -> SplitRAp in HH. rewrite SplitRMap in HH. assert (StepF_eq (ballS (StepFSup X) (proj1_sig e) ^@> a2 <@> SplitR b o) (ballS (StepFSup X) (proj1_sig e) ^@> SplitR (glue o a1 a2) o <@> SplitR b o)). { rewrite SplitRGlue. reflexivity. } rewrite H0. exact HH. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.StepFunctionSetoid CoRN.metric2.StepFunctionMonad CoRN.metric2.UniformContinuity CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.metric2.Prelength CoRN.algebra.COrdFields2 CoRN.tactics.CornTac