proposition: Lemma MirrorSplitL {X : RSetoid} : forall (s : StepF X) (a b : OpenUnit), (b == OpenUnitDual a)%Q -> (Mirror (SplitL s a)) == (SplitR (Mirror s) b).
proof: Proof. intros. apply StepF_Qeq_eq; auto with *. apply MirrorSplitL_Qeq; 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