proposition: Lemma StepQSupSplit : forall (o:OpenUnit) x, (StepQSup x == Qmax (StepQSup (SplitL x o)) (StepQSup (SplitR x o)))%Q.
proof: Proof. intros o x. revert o. induction x. intros o. change (x == Qmax x x)%Q. rewrite -> Qmax_idem. reflexivity. intros s. apply SplitLR_glue_ind; intros H. change (Qmax (StepQSup x1) (StepQSup x2) == Qmax (StepQSup (SplitL x1 (OpenUnitDiv s o H))) (Qmax (StepQSup (SplitR x1 (OpenUnitDiv s o H))) (StepQSup x2)))%Q. rewrite -> Qmax_assoc. rewrite <- IHx1. reflexivity. change (Qmax (StepQSup x1) (StepQSup x2) == Qmax (Qmax (StepQSup x1) (StepQSup (SplitL x2 (OpenUnitDualDiv s o H)))) (StepQSup (SplitR x2 (OpenUnitDualDiv s o H))))%Q. rewrite <- Qmax_assoc. rewrite <- IHx2. reflexivity. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.structures.StepQsec CoRN.metric2.Prelength CoRN.model.metric2.L1metric CoRN.model.metric2.LinfMetricMonad CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.algebra.COrdFields2 CoRN.tactics.CornTac