proposition: Lemma SplitL_resp_Xeq : forall (s1 s2 : StepF X) a, s1 == s2 -> SplitL s1 a == SplitL s2 a.
proof: Proof. induction s1. intros s2 a H. unfold StepF_eq in *. change (StepFfoldProp ((st_eqS x:X-->iffSetoid) ^@> SplitL s2 a)). rewrite <- SplitLMap. apply StepFfoldPropSplitL. assumption. intros s2 a H. destruct H using (glue_eq_ind s1_1). apply SplitL_glue_ind; intros Hao. apply StepF_eq_resp_Qeq with (SplitL s1_1 (OpenUnitDiv a o Hao)) (SplitL (SplitL s2 o) (OpenUnitDiv a o Hao)); auto. apply SplitLSplitL. simpl; field; auto with *. apply glue_StepF_eq. apply StepF_eq_resp_Qeq with s1_1 (SplitL s2 o); auto. apply StepF_Qeq_sym. apply SplitLSplitL. simpl; field; auto with *. apply StepF_eq_resp_Qeq with (SplitL s1_2 (OpenUnitDualDiv a o Hao)) (SplitL (SplitR s2 o) (OpenUnitDualDiv a o Hao)); auto. apply SplitLSplitR; simpl; field; auto with *. apply StepF_eq_resp_Qeq with s1_1 (SplitL s2 o); auto with *. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunction CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields