From: Enrico Tassi Date: Tue, 1 Jul 2008 14:25:20 +0000 (+0000) Subject: shifting done, merge attacked X-Git-Tag: make_still_working~4977 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=d03c932e859d59c0ae381f941b4003d744b6b106;hp=23dbce6cd7d599c10eb7801e91bc8b5164164418;p=helm.git shifting done, merge attacked --- diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 16d378876..69d98ade5 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,27 +1,28 @@ +sandwich.ma ordered_uniform.ma property_sigma.ma ordered_uniform.ma russell_support.ma +uniform.ma supremum.ma bishop_set.ma ordered_set.ma +sequence.ma nat/nat.ma ordered_uniform.ma uniform.ma +supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma +property_exhaustivity.ma ordered_uniform.ma property_sigma.ma bishop_set_rewrite.ma bishop_set.ma -sequence.ma nat/nat.ma +cprop_connectives.ma datatypes/constructors.ma logic/equality.ma nat_ordered_set.ma bishop_set.ma nat/compare.ma lebesgue.ma property_exhaustivity.ma sandwich.ma -property_exhaustivity.ma ordered_uniform.ma property_sigma.ma -cprop_connectives.ma datatypes/constructors.ma logic/equality.ma ordered_set.ma cprop_connectives.ma -sandwich.ma ordered_uniform.ma russell_support.ma cprop_connectives.ma nat/nat.ma -uniform.ma supremum.ma -supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma +models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma -models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma models/q_support.ma Q/q/q.ma cprop_connectives.ma -models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma -models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma -models/list_support.ma list/list.ma -models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma -models/q_function.ma models/q_bars.ma nat_ordered_set.ma models/q_bars.ma cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma +models/q_function.ma models/q_shift.ma nat_ordered_set.ma +models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma +models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma +models/q_shift.ma models/q_bars.ma +models/list_support.ma list/list.ma +models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma Q/q/q.ma datatypes/constructors.ma list/list.ma diff --git a/helm/software/matita/contribs/dama/dama/depends.png b/helm/software/matita/contribs/dama/dama/depends.png index a09d7cd89..7ce64426c 100644 Binary files a/helm/software/matita/contribs/dama/dama/depends.png and b/helm/software/matita/contribs/dama/dama/depends.png differ diff --git a/helm/software/matita/contribs/dama/dama/models/q_bars.ma b/helm/software/matita/contribs/dama/dama/models/q_bars.ma index c67bb501e..2186890f0 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -89,6 +89,25 @@ intro; elim l 0; apply le_S_S_to_le; apply H2;]] qed. +lemma sum_bases_n_m: + ∀n,m,l. + sum_bases l n < sum_bases l (S m) → + sum_bases l m < sum_bases l (S n) → + n = m. +intros 2; apply (nat_elim2 ???? n m); +[1: intro X; cases X; intros; [reflexivity] cases (?:False); + cases l in H H1; simplify; intros; + apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1)); + apply (q_lt_canc_plus_r ??? H1); +|2: intros 2; cases l; simplify; intros; cases (?:False); + apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1)); + apply (q_lt_canc_plus_r ??? H); (* magia ... *) +|3: intros 4; cases l; simplify; intros; + [1: rewrite > (H []); [reflexivity] + apply (q_lt_canc_plus_r ??(Qpos one)); assumption; + |2: rewrite > (H l1); [reflexivity] + apply (q_lt_canc_plus_r ??(Qpos (\fst b))); assumption;]] +qed. definition eject1 ≝ λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p]. @@ -254,3 +273,7 @@ intro; cases x; intros; [2:exists [apply r] reflexivity] cases (?:False); [ apply (q_lt_corefl ? H)|apply (q_neg_gt ? H)] qed. + +notation < "x \blacksquare" non associative with precedence 50 for @{'unpos $x}. +interpretation "hide unpos proof" 'unpos x = (unpos x _). + diff --git a/helm/software/matita/contribs/dama/dama/models/q_function.ma b/helm/software/matita/contribs/dama/dama/models/q_function.ma index 3275f86f0..e2187b510 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -13,118 +13,8 @@ (**************************************************************************) include "nat_ordered_set.ma". -include "models/q_bars.ma". +include "models/q_shift.ma". -lemma key: - ∀n,m,l. - sum_bases l n < sum_bases l (S m) → - sum_bases l m < sum_bases l (S n) → - n = m. -intros 2; apply (nat_elim2 ???? n m); -[1: intro X; cases X; intros; [reflexivity] cases (?:False); - cases l in H H1; simplify; intros; - apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1)); - apply (q_lt_canc_plus_r ??? H1); -|2: intros 2; cases l; simplify; intros; cases (?:False); - apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1)); - apply (q_lt_canc_plus_r ??? H); (* magia ... *) -|3: intros 4; cases l; simplify; intros; - [1: rewrite > (H []); [reflexivity] - apply (q_lt_canc_plus_r ??(Qpos one)); assumption; - |2: rewrite > (H l1); [reflexivity] - apply (q_lt_canc_plus_r ??(Qpos (\fst b))); assumption;]] -qed. - -lemma initial_shift_same_values: - ∀l1:q_f.∀init.init < start l1 → - same_values l1 - (mk_q_f init (〈\fst (unpos (start l1 - init) ?),OQ〉:: bars l1)). -[apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption] -intros; generalize in ⊢ (? ? (? ? (? ? (? ? ? (? ? ? (? ? %)) ?) ?))); intro; -cases (unpos (start l1-init) H1); intro input; -simplify in ⊢ (? ? ? (? ? ? (? ? ? (? (? ? (? ? (? ? ? % ?) ?)) ?)))); -cases (value (mk_q_f init (〈w,OQ〉::bars l1)) input) (v1 Hv1); -cases Hv1 (HV1 HV1 HV1 HV1); cases HV1 (Hi1 Hv11 Hv12); clear HV1 Hv1; -[1: cut (input < start l1) as K;[2: apply (q_lt_trans ??? Hi1 H)] - rewrite > (value_OQ_l ?? K); simplify; symmetry; assumption; -|2: cut (start l1 + sum_bases (bars l1) (len (bars l1)) ≤ input) as K;[2: - simplify in Hi1; apply (q_le_trans ???? Hi1); rewrite > H2; - rewrite > q_plus_sym in ⊢ (? ? (? ? %)); - rewrite > q_plus_assoc; rewrite > q_elim_minus; - rewrite > q_plus_sym in ⊢ (? ? (? (? ? %) ?)); - rewrite > q_plus_assoc; rewrite < q_elim_minus; - rewrite > q_plus_minus; rewrite > q_plus_sym in ⊢ (? ? (? % ?)); - rewrite > q_plus_OQ; apply q_eq_to_le; reflexivity;] - rewrite > (value_OQ_r ?? K); simplify; symmetry; assumption; -|3: simplify in Hi1; destruct Hi1; -|4: cases (q_cmp input (start l1)); - [2: rewrite > (value_OQ_l ?? H4); - change with (OQ = \snd v1); rewrite > Hv12; - cases H3; clear H3; simplify in H5; cases (\fst v1) in H5;[intros;reflexivity] - simplify; rewrite > q_d_sym; rewrite > q_d_noabs; [2:cases Hi1; apply H5] - rewrite > H2; do 2 rewrite > q_elim_minus;rewrite > q_plus_assoc; - intro X; lapply (q_le_canc_plus_r ??? X) as Y; clear X; - (* OK *) - |1,3: cases Hi1; clear Hi1; cases H3; clear H3; - simplify in H5 H6 H8 H9 H7:(? ? (? % %)) ⊢ (? ? ? (? ? ? %)); - generalize in match (refl_eq ? (bars l1):bars l1 = bars l1); - generalize in ⊢ (???% → ?); intro X; cases X; clear X; intro Hb; - [1,3: rewrite > (value_OQ_e ?? Hb); rewrite > Hv12; rewrite > Hb in Hv11 ⊢ %; - simplify in Hv11 ⊢ %; cases (\fst v1) in Hv11; [1,3:intros; reflexivity] - cases n; [1,3: intros; reflexivity] intro X; cases (not_le_Sn_O ? (le_S_S_to_le ?? X)); - |2,4: cases (value_ok l1 input); - [1,5: rewrite > Hv12; rewrite > Hb; clear Hv12; simplify; - rewrite > H10; rewrite > Hb; - cut (O < \fst v1);[2,4: cases (\fst v1) in H9; intros; [2,4: autobatch] - cases (?:False); generalize in match H9; - rewrite > q_d_sym; rewrite > q_d_noabs; [2,4: assumption] - rewrite > H2; simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ; - repeat rewrite > q_elim_minus; - intro X; lapply (q_lt_canc_plus_r ??? X) as Y; - apply (q_lt_le_incompat ?? Y); - [apply q_eq_to_le;symmetry|apply q_lt_to_le] assumption;] - cases (\fst v1) in H8 H9 Hcut; [1,3:intros (_ _ X); cases (not_le_Sn_O ? X)] - intros; clear H13; simplify; - rewrite > (key n n1 (b::l)); [1,4: reflexivity] rewrite < Hb; - [2,4: simplify in H8; apply (q_le_lt_trans ??? (q_le_plus_r ??? H8)); - apply (q_le_lt_trans ???? H12); rewrite > H2; - rewrite > q_d_sym; rewrite > q_d_noabs; [2,4: assumption] - rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib; - rewrite > q_elim_opp; repeat rewrite > q_elim_minus; - rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init); - rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? (? % ?) ?); - rewrite > (q_plus_sym ? init); do 2 rewrite < q_elim_minus; - rewrite > q_plus_minus; rewrite > q_plus_OQ; - rewrite > q_d_sym; rewrite > q_d_noabs; - [2,4: [apply q_eq_to_le; symmetry|apply q_lt_to_le] assumption] - apply q_eq_to_le; reflexivity; - |*: apply (q_le_lt_trans ??? H11); - rewrite > q_d_sym; rewrite > q_d_noabs; - [2,4: [apply q_eq_to_le; symmetry|apply q_lt_to_le] assumption] - generalize in match H9; rewrite > q_d_sym; rewrite > q_d_noabs; - [2,4: assumption] - rewrite > H2; intro X; - lapply (q_lt_inj_plus_r ?? (Qopp (start l1-init)) X) as Y; clear X; - rewrite < q_plus_assoc in Y; repeat rewrite < q_elim_minus in Y; - rewrite > q_plus_minus in Y; rewrite > q_plus_OQ in Y; - apply (q_le_lt_trans ???? Y); - rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib; - rewrite > q_elim_opp; repeat rewrite > q_elim_minus; - rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init); - rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? ? (? % ?)); - rewrite > (q_plus_sym ? init); rewrite < (q_elim_minus init); - rewrite > q_plus_minus; rewrite > q_plus_OQ; - apply q_eq_to_le; reflexivity;] - |2,6: rewrite > Hb; intro W; destruct W; - |3,7: [apply q_eq_to_le;symmetry|apply q_lt_to_le] assumption; - |4,8: apply (q_lt_le_trans ??? H7); rewrite > H2; - rewrite > q_plus_sym; rewrite < q_plus_assoc; - rewrite > q_plus_sym; apply q_le_inj_plus_r; - apply q_le_minus; apply q_eq_to_le; reflexivity;]]] -qed. - - - alias symbol "pi2" = "pair pi2". alias symbol "pi1" = "pair pi1". definition rebase_spec ≝ @@ -206,23 +96,40 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec; [1: reflexivity |2: assumption; |3: assumption; - |4: intro; rewrite < (H4 input); clear H3 H4 H2 w; - cases (value (mk_q_f s1 l2') input); - cases (q_cmp input (start (mk_q_f s1 l2'))) in H1; - whd in ⊢ (% → ?); - [1: intros; cases H2; clear H2; whd in ⊢ (??? %); - cases (value (mk_q_f s2 l2) input); - cases (q_cmp input (start (mk_q_f s2 l2))) in H2; - whd in ⊢ (% → ?); - [1: intros; cases H6; clear H6; change with (w1 = w); - - (* TODO *) ]] + |4: intro; rewrite > (initial_shift_same_values (mk_q_f s2 l2) s1 H input); + rewrite < (H4 input); reflexivity;] + |3: letin l1' ≝ (〈\fst (unpos (s1-s2) ?),OQ〉::l1);[ + apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; + assumption] + cases (aux l1' l2 (S (len l1' + len l2))); + cases (H1 s2 (le_n ?)); clear H1 aux; + exists [apply 〈mk_q_f s2 (\fst w), mk_q_f s2 (\snd w)〉] split; + [1: reflexivity + |2: assumption; + |4: assumption; + |3: intro; rewrite > (initial_shift_same_values (mk_q_f s1 l1) s2 H input); + rewrite < (H3 input); reflexivity;]] |1,2: unfold rest; apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption; -|3:(* TODO *) -|4:(* TODO *) -|5:(* TODO *) -|6:(* TODO *) -|7:(* TODO *) -|8: intros; cases (?:False); apply (not_le_Sn_O ? H1);] +|8: intros; cases (?:False); apply (not_le_Sn_O ? H1); +|3: intros; generalize in match (unpos ??); intro X; cases X; clear X; + simplify in ⊢ (???? (??? (??? (??? (?? (? (?? (??? % ?) ?) ??)))) ?)); + simplify in ⊢ (???? (???? (??? (??? (?? (? (?? (??? % ?) ?) ??)))))); + clear H4; cases (aux (〈w,\snd b〉::l4) l5 n1); clear aux; + cut (len (〈w,\snd b〉::l4) + len l5 < n1) as K;[2: + simplify in H5; simplify; rewrite > sym_plus in H5; simplify in H5; + rewrite > sym_plus in H5; apply le_S_S_to_le; apply H5;] + split; + [1: simplify in ⊢ (? % ?); simplify in ⊢ (? ? %); + cases (H4 s K); clear K H4; intro input; cases input; [reflexivity] + simplify; apply H7; + |2: simplify in ⊢ (? ? %); cases (H4 s K); clear H4 K H5 spec; + intro; + (* input < s + b1 || input >= s + b1 *) + |3: simplify in ⊢ (? ? %);] +|4: intros; generalize in match (unpos ??); intro X; cases X; clear X; + (* duale del 3 *) +|5: intros; (* triviale, caso in cui non fa nulla *) +|6,7: (* casi base in cui allunga la lista più corta *) +] qed. diff --git a/helm/software/matita/contribs/dama/dama/models/q_shift.ma b/helm/software/matita/contribs/dama/dama/models/q_shift.ma new file mode 100644 index 000000000..f247fb11d --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/models/q_shift.ma @@ -0,0 +1,105 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "models/q_bars.ma". + +lemma initial_shift_same_values: + ∀l1:q_f.∀init.init < start l1 → + same_values l1 + (mk_q_f init (〈\fst (unpos (start l1 - init) ?),OQ〉:: bars l1)). +[apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption] +intros; generalize in ⊢ (? ? (? ? (? ? (? ? ? (? ? ? (? ? %)) ?) ?))); intro; +cases (unpos (start l1-init) H1); intro input; +simplify in ⊢ (? ? ? (? ? ? (? ? ? (? (? ? (? ? (? ? ? % ?) ?)) ?)))); +cases (value (mk_q_f init (〈w,OQ〉::bars l1)) input) (v1 Hv1); +cases Hv1 (HV1 HV1 HV1 HV1); cases HV1 (Hi1 Hv11 Hv12); clear HV1 Hv1; +[1: cut (input < start l1) as K;[2: apply (q_lt_trans ??? Hi1 H)] + simplify in ⊢ (? ? ? (? ? ? %)); + rewrite > (value_OQ_l ?? K); simplify; symmetry; assumption; +|2: cut (start l1 + sum_bases (bars l1) (len (bars l1)) ≤ input) as K;[2: + simplify in Hi1; apply (q_le_trans ???? Hi1); rewrite > H2; + rewrite > q_plus_sym in ⊢ (? ? (? ? %)); + rewrite > q_plus_assoc; rewrite > q_elim_minus; + rewrite > q_plus_sym in ⊢ (? ? (? (? ? %) ?)); + rewrite > q_plus_assoc; rewrite < q_elim_minus; + rewrite > q_plus_minus; rewrite > q_plus_sym in ⊢ (? ? (? % ?)); + rewrite > q_plus_OQ; apply q_eq_to_le; reflexivity;] + simplify in ⊢ (? ? ? (? ? ? %)); + rewrite > (value_OQ_r ?? K); simplify; symmetry; assumption; +|3: simplify in Hi1; destruct Hi1; +|4: cut (start l1 ≤ input → \snd (\fst (value l1 input))=\snd v1) as solution;[2: + intro H4; cases Hi1; clear Hi1; cases H3; clear H3; + simplify in H5 H6 H8 H9 H7:(? ? (? % %)) ⊢ (? ? ? (? ? ? %)); + generalize in match (refl_eq ? (bars l1):bars l1 = bars l1); + generalize in ⊢ (???% → ?); intro X; cases X; clear X; intro Hb; + [1: rewrite > (value_OQ_e ?? Hb); rewrite > Hv12; rewrite > Hb in Hv11 ⊢ %; + simplify in Hv11 ⊢ %; cases (\fst v1) in Hv11; [intros; reflexivity] + cases n; [intros; reflexivity] intro X; cases (not_le_Sn_O ? (le_S_S_to_le ?? X)); + |2: cases (value_ok l1 input); + [2: rewrite > Hb; intro W; destruct W; + |3: assumption; + |4: apply (q_lt_le_trans ??? H7); rewrite > H2; + rewrite > q_plus_sym; rewrite < q_plus_assoc; + rewrite > q_plus_sym; apply q_le_inj_plus_r; + apply q_le_minus; apply q_eq_to_le; reflexivity; + |1: rewrite > Hv12; rewrite > Hb; clear Hv12; simplify; + rewrite > H10; rewrite > Hb; + cut (O < \fst v1);[2: cases (\fst v1) in H9; intros; [2: autobatch] + cases (?:False); generalize in match H9; + rewrite > q_d_sym; rewrite > q_d_noabs; [2,4: assumption] + rewrite > H2; simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ; + repeat rewrite > q_elim_minus; + intro X; lapply (q_lt_canc_plus_r ??? X) as Y; + apply (q_lt_le_incompat ?? Y); assumption;] + cases (\fst v1) in H8 H9 Hcut; [1:intros (_ _ X); cases (not_le_Sn_O ? X)] + intros; clear H13; simplify; + rewrite > (sum_bases_n_m n n1 (b::l)); [1,4: reflexivity] rewrite < Hb; + [2: simplify in H8; apply (q_le_lt_trans ??? (q_le_plus_r ??? H8)); + apply (q_le_lt_trans ???? H12); rewrite > H2; + rewrite > q_d_sym; rewrite > q_d_noabs; [2: assumption] + rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib; + rewrite > q_elim_opp; repeat rewrite > q_elim_minus; + rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init); + rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? (? % ?) ?); + rewrite > (q_plus_sym ? init); do 2 rewrite < q_elim_minus; + rewrite > q_plus_minus; rewrite > q_plus_OQ; + rewrite > q_d_sym; rewrite > q_d_noabs; [2:assumption] + apply q_eq_to_le; reflexivity; + |*: apply (q_le_lt_trans ??? H11); + rewrite > q_d_sym; rewrite > q_d_noabs; [2:assumption;] + generalize in match H9; rewrite > q_d_sym; rewrite > q_d_noabs; [2: assumption] + rewrite > H2; intro X; + lapply (q_lt_inj_plus_r ?? (Qopp (start l1-init)) X) as Y; clear X; + rewrite < q_plus_assoc in Y; repeat rewrite < q_elim_minus in Y; + rewrite > q_plus_minus in Y; rewrite > q_plus_OQ in Y; + apply (q_le_lt_trans ???? Y); + rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib; + rewrite > q_elim_opp; repeat rewrite > q_elim_minus; + rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init); + rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? ? (? % ?)); + rewrite > (q_plus_sym ? init); rewrite < (q_elim_minus init); + rewrite > q_plus_minus; rewrite > q_plus_OQ; + apply q_eq_to_le; reflexivity;]]]]] + cases (q_cmp input (start l1)); + [2: simplify in ⊢ (? ? ? (? ? ? %)); rewrite > (value_OQ_l ?? H4); + change with (OQ = \snd v1); rewrite > Hv12; + cases H3; clear H3; simplify in H5; cases (\fst v1) in H5;[intros;reflexivity] + simplify; rewrite > q_d_sym; rewrite > q_d_noabs; [2:cases Hi1; apply H5] + rewrite > H2; do 2 rewrite > q_elim_minus;rewrite > q_plus_assoc; + intro X; lapply (q_le_canc_plus_r ??? X) as Y; clear X; + cases (?:False); apply (q_lt_le_incompat input (start l1)); try assumption; + apply (q_le_S ???? Y); try assumption; apply sum_bases_ge_OQ; + |1: apply solution; apply (q_eq_to_le ?? (sym_eq ??? H4)); + |3: apply solution; apply (q_lt_to_le ?? H4);] +qed.