proposition: Lemma SplitMap (X Y:Type):forall x:(StepF X), forall a, forall f:X->Y, (Split (Map f x) a) = let (l,r) := Split x a in (Map f l,Map f r).
proof: Proof. intros s a f. revert a. induction s. simpl; auto. intros a. simpl. destruct (Q_dec a o) as [[H0|H0]|H0]. rewrite IHs1. destruct (Split s1 (OpenUnitDiv a o H0)). auto with *. rewrite IHs2. destruct (Split s2 (OpenUnitDualDiv a o H0)). auto with *. auto. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields