rewrite < sym_Rplus;apply Rle_minus_r_to_l;
apply (pos_z_to_le_Rtimes_Rtimes_to_lt ? ? (n*Rexp_nat a (n-1)))
[apply pos_times_pos_pos
- [lapply (nat_lt_to_R_lt ?? H1);autobatch
+ [apply (nat_lt_to_R_lt ?? H1);
|elim daemon]
|rewrite > Rtimes_x_R0;do 2 rewrite > distr_Rtimes_Rplus_l;
rewrite > sym_Rtimes in ⊢ (? ? (? (? ? (? ? (? %))) ?));
rewrite < distr_Rtimes_Rplus_l;
apply (trans_Rle ? (Rexp_nat a n - Rexp_nat y n))
[apply Rle_plus_l;left;autobatch
- |rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%));
+ | cut (∀x,y.(S x ≤ y) = (x < y));[2: intros; reflexivity]
+ (* applyS Rexp_nat_tech by sym_Rtimes, assoc_Rtimes;*)
+ rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%));
rewrite < assoc_Rtimes;apply Rexp_nat_tech
[autobatch
|assumption
|(* by transitivity y^n < x < a^n and injectivity *) elim daemon]]
|intro;apply (irrefl_Rlt (n*Rexp_nat a (n-1)));
rewrite > H11 in ⊢ (?%?);apply pos_times_pos_pos
- [lapply (nat_lt_to_R_lt ?? H1);autobatch
+ [apply (nat_lt_to_R_lt ?? H1);
|elim daemon]]]]
|elim (R_archimedean R1 ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1))))
[|autobatch]
assumption
|apply lt_R0_Rinv;apply pos_times_pos_pos
[apply pos_times_pos_pos
- [lapply (nat_lt_to_R_lt ?? H1);autobatch
+ [apply (nat_lt_to_R_lt ?? H1);
|elim daemon]
|apply (trans_Rlt ???? H8);apply pos_times_pos_pos
[apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0;
assumption
|apply lt_R0_Rinv;apply pos_times_pos_pos
- [lapply (nat_lt_to_R_lt ?? H1);autobatch
+ [apply (nat_lt_to_R_lt ?? H1);
|elim daemon]]]]]
|split
[(* show that h > R0, also useful in previous parts of the proof *)
|simplify;cases z;simplify
[1,3:autobatch
|rewrite < plus_n_O;rewrite > plus_n_O in ⊢ (?%?);
- apply lt_plus;autobatch]
+ apply lt_plus;autobatch depth=2]
|simplify;cases z;simplify;
[1,3:autobatch
|rewrite < plus_n_O;rewrite > (times_n_O O) in ⊢ (?%?);
lemma root_root_times : ∀x,n,m,H,H1,H2.root m (root n x H H1) H2 ? =
root (m*n) x ? H1.
[cases (root_sound n x H H1);assumption
-|autobatch
+| change in match O with (O*O); apply lt_times; assumption;
+ (* autobatch paramodulation; non fa narrowing, non fa deep subsumption... *)
|intros;lapply (Rexp_nat_Rexp_nat_Rtimes (root m (root n x H H1) H2 ?) m n)
[cases (root_sound n x H H1);assumption
|cases (root_sound m (root n x H H1))