proposition: Lemma SplitGlue : forall x y:StepF, forall o, (Split (glue o x y) o)=(x, y).
proof: Proof. intros. simpl. destruct (Q_dec o o) as [[H1|H1]|H1]; try (elim (Qlt_not_le _ _ H1); auto with * ); simpl; auto with *. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields