-(*
-lemma lt_n_plus_n_Sm : ∀n,m:nat.n < n + S m.
-intros; rewrite > sym_plus; apply (le_S_S n (m+n)); apply (le_plus_n m n); qed.
-*)
-
-(*
-lemma all_bigger_can_concat_bigger:
- ∀l1,l2,start,b,x,n.
- (∀i.i< len l1 → nth_base l1 i < \fst b) →
- (∀i.i< len l2 → \fst b ≤ nth_base l2 i) →
- (∀i.i< len l1 → start ≤ i → x ≤ nth_base l1 i) →
- start ≤ n → n < len (l1@b::l2) → x ≤ \fst b → x ≤ nth_base (l1@b::l2) n.
-intros; cases (cmp_nat n (len l1));
-[1: unfold nth_base; rewrite > (nth_concat_lt_len ????? H6);
- apply (H2 n); assumption;
-|2: rewrite > H6; unfold nth_base; rewrite > nth_len; assumption;
-|3: unfold nth_base; rewrite > nth_concat_ge_len; [2: apply lt_to_le; assumption]
- rewrite > len_concat in H4; simplify in H4; rewrite < plus_n_Sm in H4;
- lapply linear le_S_S_to_le to H4 as K; rewrite > sym_plus in K;
- lapply linear le_plus_to_minus to K as X;
- generalize in match X; generalize in match (n - len l1); intro W; cases W; clear W X;
- [intros; assumption] intros;
- apply (q_le_trans ??? H5); apply (H1 n1); assumption;]
-qed.
-*)
-
-
-inductive value_spec (f : q_f) (i : ℚ) : ℚ → nat → CProp ≝
- value_of : ∀q,j.
- nth_height (bars f) j = q →
- nth_base (bars f) j < i →
- (∀n.j < n → n < \len (bars f) → i ≤ nth_base (bars f) n) → value_spec f i q j.
-
-
-inductive break_spec (T : Type) (n : nat) (l : list T) : list T → CProp ≝
-| break_to: ∀l1,x,l2. \len l1 = n → l = l1 @ [x] @ l2 → break_spec T n l l.
-
-lemma list_break: ∀T,n,l. n < \len l → break_spec T n l l.
-intros 2; elim n;
-[1: elim l in H; [cases (not_le_Sn_O ? H)]
- apply (break_to ?? ? [] a l1); reflexivity;
-|2: cases (H l); [2: apply lt_S_to_lt; assumption;] cases l2 in H3; intros;
- [1: rewrite < H2 in H1; rewrite > H3 in H1; rewrite > append_nil in H1;
- rewrite > len_append in H1; rewrite > plus_n_SO in H1;
- cases (not_le_Sn_n ? H1);
- |2: apply (break_to ?? ? (l1@[x]) t l3);
- [2: simplify; rewrite > associative_append; assumption;
- |1: rewrite < H2; rewrite > len_append; rewrite > plus_n_SO; reflexivity]]]
-qed.
-
-definition value : ∀f:q_f.∀i:ratio.∃p:ℚ.∃j.value_spec f (Qpos i) p j.
-intros;
-letin P ≝
- (λx:bar.match q_cmp (Qpos i) (\fst x) with[ q_leq _ ⇒ true| q_gt _ ⇒ false]);
-exists [apply (nth_height (bars f) (pred (find ? P (bars f) ▭)));]
-exists [apply (pred (find ? P (bars f) ▭))] apply value_of;
+alias symbol "lt" (instance 9) = "Q less than".
+alias symbol "lt" (instance 7) = "natural 'less than'".
+alias symbol "lt" (instance 6) = "natural 'less than'".
+alias symbol "lt" (instance 5) = "Q less than".
+alias symbol "lt" (instance 4) = "natural 'less than'".
+alias symbol "lt" (instance 2) = "natural 'less than'".
+alias symbol "leq" = "Q less or equal than".
+coinductive value_spec (f : list bar) (i : ℚ) : ℚ × ℚ → CProp ≝
+| value_of : ∀j,q.
+ nth_height f j = q → nth_base f j < i → j < \len f →
+ (∀n.n<j → nth_base f n < i) →
+ (∀n.j < n → n < \len f → i ≤ nth_base f n) → value_spec f i q.
+
+definition match_pred ≝
+ λi.λx:bar.match q_cmp (Qpos i) (\fst x) with[ q_leq _ ⇒ true| q_gt _ ⇒ false].
+
+definition match_domain ≝
+ λf: list bar.λi:ratio. pred (find ? (match_pred i) f ▭).
+
+definition value_simple ≝
+ λf: list bar.λi:ratio. nth_height f (match_domain f i).
+
+alias symbol "lt" (instance 5) = "Q less than".
+alias symbol "lt" (instance 6) = "natural 'less than'".
+definition value_lemma :
+ ∀f:list bar.sorted q2_lt f → O < length bar f →
+ ∀i:ratio.nth_base f O < Qpos i → ∃p:ℚ×ℚ.value_spec f (Qpos i) p.
+intros (f bars_sorted_f len_bases_gt_O_f i bars_begin_OQ_f);
+exists [apply (value_simple f i);]
+apply (value_of ?? (match_domain f i));