+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.
+
+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,x.sum_bases l x < sum_bases l (S x).
+intro; elim l;
+[1: elim x;
+ [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ;
+ apply q_pos_lt_OQ;
+ |2: simplify in H ⊢ %;
+ apply q_lt_plus; rewrite > q_elim_minus;
+ rewrite < q_plus_assoc; rewrite < q_elim_minus;
+ rewrite > q_plus_minus; rewrite > q_plus_OQ;
+ assumption;]
+|2: elim x;
+ [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ;
+ apply q_pos_lt_OQ;
+ |2: simplify; change in ⊢ (? ? (? % ?)) with (sum_bases l1 (S n)) ;
+ apply q_lt_plus; rewrite > q_elim_minus;
+ rewrite < q_plus_assoc; rewrite < q_elim_minus;
+ rewrite > q_plus_minus; rewrite > q_plus_OQ; apply H]]
+qed.
+
+lemma sum_bases_lt_canc:
+ ∀l,x,y.sum_bases l (S x) < sum_bases l (S y) → sum_bases l x < sum_bases l y.
+intro; elim l; [apply (q_lt_canc_plus_r ?? (Qpos one));apply H]
+generalize in match H1;apply (nat_elim2 (?:? → ? → CProp) ??? x y);
+intros 2;
+[3: intros 2; simplify; apply q_lt_inj_plus_r; apply H;
+ apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H3;
+|2: cases (?:False); simplify in H2;
+ apply (q_lt_le_incompat (sum_bases l1 (S n)) OQ);[2: apply sum_bases_ge_OQ;]
+ apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H2;
+|1: cases n in H2; intro;
+ [1: cases (?:False); apply (q_lt_corefl ? H2);
+ |2: simplify; apply q_lt_plus_trans; [apply sum_bases_ge_OQ]
+ apply q_pos_lt_OQ;]]
+qed.
+
+lemma sum_bars_increasing2:
+ ∀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;]]
+qed.
+