proposition: Lemma IntegralSplit : forall (o:OpenUnit) x, (IntegralQ x == affineCombo o (IntegralQ (SplitL x o)) (IntegralQ (SplitR x o)))%Q.
proof: Proof. intros o x. revert o. induction x. unfold IntegralQ. simpl. intros. unfold affineCombo; simpl in x; ring. intros p. rewrite -> Integral_glue. apply SplitLR_glue_ind; intros H. rewrite -> Integral_glue. unfold affineCombo in *. rewrite -> (IHx1 (OpenUnitDiv p o H)). unfold IntegralQ; simpl; fold IntegralQ. unfold affineCombo; field; auto with *. rewrite -> Integral_glue. simpl. unfold IntegralQ; simpl; fold IntegralQ. repeat rewrite Qred_correct. unfold affineCombo in *. rewrite -> (IHx2 (OpenUnitDualDiv p o H)). unfold IntegralQ; simpl; fold IntegralQ. unfold affineCombo; field; auto with *. unfold affineCombo in *. rewrite -> H. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.structures.StepQsec CoRN.metric2.UniformContinuity CoRN.metric2.Prelength 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