+
+include "Q/q/qtimes.ma".
+
+let rec area (l:list bar) on l ≝
+ match l with
+ [ nil ⇒ OQ
+ | cons he tl ⇒ area tl + Qpos (\fst he) * ⅆ[OQ,\snd he]].
+
+alias symbol "pi1" = "exT \fst".
+alias symbol "minus" = "Q minus".
+alias symbol "exists" = "CProp exists".
+definition minus_spec_bar ≝
+ λf,g,h:list bar.
+ same_bases f g → len f = len g →
+ ∀s,i:ℚ. \snd (\fst (value (mk_q_f s h) i)) =
+ \snd (\fst (value (mk_q_f s f) i)) - \snd (\fst (value (mk_q_f s g) i)).
+
+definition minus_spec ≝
+ λf,g:q_f.
+ ∃h:q_f.
+ ∀i:ℚ. \snd (\fst (value h i)) =
+ \snd (\fst (value f i)) - \snd (\fst (value g i)).
+
+definition eject_bar : ∀P:list bar → CProp.(∃l:list bar.P l) → list bar ≝
+ λP.λp.match p with [ex_introT x _ ⇒ x].
+definition inject_bar ≝ ex_introT (list bar).
+
+coercion inject_bar with 0 1 nocomposites.
+coercion eject_bar with 0 0 nocomposites.
+
+lemma minus_q_f : ∀f,g. minus_spec f g.
+intros;
+letin aux ≝ (
+ let rec aux (l1, l2 : list bar) on l1 ≝
+ match l1 with
+ [ nil ⇒ []
+ | cons he1 tl1 ⇒
+ match l2 with
+ [ nil ⇒ []
+ | cons he2 tl2 ⇒ 〈\fst he1, \snd he1 - \snd he2〉 :: aux tl1 tl2]]
+ in aux : ∀l1,l2 : list bar.∃h.minus_spec_bar l1 l2 h);
+[2: intros 4; simplify in H3; destruct H3;
+|3: intros 4; simplify in H3; cases l1 in H2; [2: intro X; simplify in X; destruct X]
+ intros; rewrite > (value_OQ_e (mk_q_f s []) i); [2: reflexivity]
+ rewrite > q_elim_minus; rewrite > q_plus_OQ; reflexivity;
+|1: cases (aux l2 l3); unfold in H2; intros 4;
+ simplify in ⊢ (? ? (? ? ? (? ? ? (? % ?))) ?);
+ cases (q_cmp i (s + Qpos (\fst b)));
+
+
+
+definition excess ≝
+ λf,g.∃i.\snd (\fst (value f i)) < \snd (\fst (value g i)).
+