-interpretation "lq2" 'lq2 = (list bar).
-
-let rec sum_bases (l:list bar) (i:nat) on i ≝
- match i with
- [ O ⇒ OQ
- | S m ⇒
- match l with
- [ nil ⇒ sum_bases [] m + Qpos one
- | cons x tl ⇒ sum_bases tl m + Qpos (\fst x)]].
-
-axiom sum_bases_empty_nat_of_q_ge_OQ:
- ∀q:ℚ.OQ ≤ sum_bases [] (nat_of_q q).
-axiom sum_bases_empty_nat_of_q_le_q:
- ∀q:ℚ.sum_bases [] (nat_of_q q) ≤ q.
-axiom sum_bases_empty_nat_of_q_le_q_one:
- ∀q:ℚ.q < sum_bases [] (nat_of_q q) + Qpos one.
-
-lemma sum_bases_ge_OQ:
- ∀l,n. OQ ≤ sum_bases l n.
-intro; elim l; simplify; intros;
-[1: elim n; [apply q_eq_to_le;reflexivity] simplify;
- apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ;
-|2: cases n; [apply q_eq_to_le;reflexivity] simplify;
- apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]]
-qed.
-
-alias symbol "leq" = "Q less or equal than".
-lemma sum_bases_O:
- ∀l.∀x.sum_bases l x ≤ OQ → x = O.
-intros; cases x in H; [intros; reflexivity] intro; cases (?:False);
-cases (q_le_cases ?? H);
-[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %);
-|2: apply (q_lt_antisym ??? H1);] clear H H1; cases l;
-simplify; apply q_lt_plus_trans;
-try apply q_pos_lt_OQ;
-try apply (sum_bases_ge_OQ []);
-apply (sum_bases_ge_OQ l1);
-qed.
-
-
-lemma sum_bases_increasing:
- ∀l.∀n1,n2:nat.n1<n2→sum_bases l n1 < sum_bases l n2.
-intro; elim l 0;
-[1: intros 2; apply (cic:/matita/dama/nat_ordered_set/nat_elim2.con ???? n1 n2);
- [1: intro; cases n;
- [1: intro X; cases (not_le_Sn_O ? X);
- |2: simplify; intros; apply q_lt_plus_trans;
- [1: apply sum_bases_ge_OQ;|2: apply (q_pos_lt_OQ one)]]
- |2: simplify; intros; cases (not_le_Sn_O ? H);
- |3: simplify; intros; apply q_lt_inj_plus_r;
- apply H; apply le_S_S_to_le; apply H1;]
-|2: intros 5; apply (cic:/matita/dama/nat_ordered_set/nat_elim2.con ???? n1 n2);
- [1: simplify; intros; cases n in H1; intros;
- [1: cases (not_le_Sn_O ? H1);
- |2: simplify; apply q_lt_plus_trans;
- [1: apply sum_bases_ge_OQ;|2: apply q_pos_lt_OQ]]
- |2: simplify; intros; cases (not_le_Sn_O ? H1);
- |3: simplify; intros; apply q_lt_inj_plus_r; apply H;
- apply le_S_S_to_le; apply H2;]]
+interpretation "lq2" 'lq2 = (list bar).
+
+inductive sorted : list bar → Prop ≝
+| sorted_nil : sorted []
+| sorted_one : ∀x. sorted [x]
+| sorted_cons : ∀x,y,tl. \fst x < \fst y → sorted (y::tl) → sorted (x::y::tl).
+
+definition nth_base ≝ λf,n. \fst (nth f ▭ n).
+definition nth_height ≝ λf,n. \snd (nth f ▭ n).
+
+record q_f : Type ≝ {
+ bars: list bar;
+ increasing_bars : sorted bars;
+ bars_begin_OQ : nth_base bars O = OQ;
+ bars_tail_OQ : nth_height bars (pred (len bars)) = OQ
+}.
+
+lemma nth_nil: ∀T,i.∀def:T. nth [] def i = def.
+intros; elim i; simplify; [reflexivity;] assumption; qed.
+
+lemma all_bases_positives : ∀f:q_f.∀i.i < len (bars f) → OQ < nth_base (bars f) i.
+intro f; elim (increasing_bars f);
+[1: unfold nth_base; rewrite > nth_nil; apply (q_pos_OQ one);
+|2: cases i in H; [2: cases (?:False);