proposition: Lemma SplitRBind (X Y : RSetoid) : forall (y:(StepF X)) (o:OpenUnit) (f: (X-->(StepFS Y))), SplitR (StFBind00 y f) o == StFBind00 (SplitR y o) (compose1 (SplitRS Y o) f).
proof: Proof. induction y. reflexivity. intros p f. simpl. apply SplitR_glue_ind; apply SplitR_glue_ind; intros H H0; try solve [ elim (Qlt_not_le o p); auto with * | elim (Qlt_not_le _ _ H0) || elim (Qlt_not_le _ _ H); rewrite -> H || rewrite -> H0; auto with *]. simpl. apply glue_wd. unfold ou_eq; reflexivity. setoid_replace (OpenUnitDiv _ _ H0) with (OpenUnitDiv _ _ H) by (unfold ou_eq; reflexivity). rewrite -> IHy1. apply StFBind_wd1. intro. simpl. unfold compose0, SplitLS0, SplitRS0. symmetry. apply StepF_Qeq_eq. apply ((SplitLSplitR (f x) p) (OpenUnitDualDiv _ _ H)); simpl; field; auto with *. apply StFBind_wd1. intro x. simpl. unfold compose0, SplitLS0. symmetry. apply: (@StepF_Qeq_eq). apply (SplitRSplitR (f x)). simpl. field. auto with *. setoid_replace (OpenUnitDualDiv p o H0) with (OpenUnitDualDiv p o H) by (unfold ou_eq; reflexivity). rewrite -> IHy2. apply StFBind_wd1. intros x. simpl. unfold compose0. apply StepF_Qeq_eq. apply (SplitRSplitR (f x) o (OpenUnitDualDiv _ _ H) p). simpl. field. auto with *. apply StFBind_wd1. intro. simpl. unfold compose0, SplitLS0, SplitRS0. apply SplitR_wd;auto with *. symmetry. auto with *. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunctionSetoid CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.logic.CornBasics