proposition: Lemma glue_injr {X:RSetoid} :forall o (x y x1 y1:StepF X), (glue o x y)==(glue o x1 y1) -> (y==y1).
proof: Proof. intros. destruct H as [_ H] using (glue_eq_ind x). rewrite SplitRGlue in H. assumption. 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