proposition: Lemma int_add (a b c : Q) : int a b + int b c = int a c.
proof: Proof. unfold int. destruct (decide (a ≤ b)) as [AB | AB]; destruct (decide (b ≤ c)) as [BC | BC]; destruct (decide (a ≤ c)) as [AC | AC]. + apply integral_additive'; simpl; ring. + assert (A : a ≤ c) by (now transitivity b); elim (AC A). + apply minus_eq_plus. symmetry. pose proof (integral_additive' a c ((c - a) ↾ int_obligation_1 a c AC) ((b - c) ↾ int_obligation_2 b c BC) ((b - a) ↾ int_obligation_1 a b AB) ). apply H0. clear H0. simpl. ring. simpl. ring. + apply minus_eq_plus. rewrite (rings.plus_comm (-integrate _ _ _)), <- plus_eq_minus, (rings.plus_comm (integrate _ _ _)). pose proof (integral_additive' c a ((a - c) ↾ int_obligation_2 a c AC) ((b - a) ↾ int_obligation_1 a b AB) ((b - c) ↾ int_obligation_2 b c BC) ). apply H0. clear H0. simpl. ring. simpl. ring. + rewrite (rings.plus_comm (-integrate _ _ _)). apply minus_eq_plus. rewrite (rings.plus_comm (integrate _ _ _)). symmetry. pose proof (integral_additive' b a ((a - b) ↾ int_obligation_2 a b AB) ((c - a) ↾ int_obligation_1 a c AC) ((c - b) ↾ int_obligation_1 b c BC) ). apply H0. clear H0. simpl. ring. simpl. ring. + rewrite (rings.plus_comm (-integrate _ _ _)). apply minus_eq_plus. rewrite (rings.plus_comm (-integrate _ _ _)), <- plus_eq_minus. pose proof (integral_additive' b c ((c - b) ↾ int_obligation_1 b c BC) ((a - c) ↾ int_obligation_2 a c AC) ((a - b) ↾ int_obligation_2 a b AB) ). apply H0. clear H0. simpl. ring. simpl. ring. + assert (b ≤ a) by (now apply orders.le_flip); assert (B : b ≤ c) by (now transitivity a); elim (BC B). + rewrite <- rings.negate_plus_distr. apply negate_inj. rewrite (rings.plus_comm (integrate _ _ _)). pose proof (integral_additive' c b ((b - c) ↾ int_obligation_2 b c BC) ((a - b) ↾ int_obligation_2 a b AB) ((a - c) ↾ int_obligation_2 a c AC) ). apply H0. clear H0. simpl. ring. simpl. ring. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal Coq.Unicode.Utf8 Coq.Program.Program CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.Qmetric CoRN.stdlib_omissions.P CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q CoRN.stdlib_omissions.N CoRN.ode.metric CoRN.ode.FromMetric2 CoRN.ode.SimpleIntegration MathClasses.misc.propholds