proposition: Lemma SplitRMap(X Y:Type): forall x:(StepF X), forall a, forall f:X->Y, SplitR (Map f x) a = Map f (SplitR x a).
proof: Proof. intros. unfold SplitR. rewrite SplitMap. destruct (Split x a). simpl. auto. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields