+ ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)).
+
+definition same_bases ≝
+ λl1,l2:q_f.
+ (∀i.\fst (nth (bars l1) ▭ i) = \fst (nth (bars l2) ▭ i)).
+
+axiom q_lt_corefl: ∀x:Q.x < x → False.
+axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False.
+axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False.
+axiom q_d_x_x: ∀x:Q.ⅆ[x,x] = OQ.
+axiom q_pos_OQ: ∀x.Qpos x ≤ OQ → False.
+axiom q_lt_plus_trans:
+ ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y.
+axiom q_pos_lt_OQ: ∀x.OQ < Qpos x.
+axiom q_le_plus_trans:
+ ∀x,y:Q. OQ ≤ x → OQ ≤ y → OQ ≤ x + y.
+
+lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.
+intro; cases x; intros; [2:exists [apply r] reflexivity]
+cases (?:False);
+[ apply (q_lt_corefl ? H)|apply (q_neg_gt ? H)]
+qed.
+
+notation < "\blacksquare" non associative with precedence 90 for @{'hide}.
+definition hide ≝ λT:Type.λx:T.x.
+interpretation "hide" 'hide = (hide _ _).
+
+lemma sum_bases_ge_OQ:
+ ∀l,n. OQ ≤ sum_bases (bars l) n.
+intro; elim (bars l); simplify; intros;
+[1: elim n; [left;reflexivity] simplify;
+ apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ;
+|2: cases n; [left;reflexivity] simplify;
+ apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]]
+qed.