apply (trans_Rle ? (Rexp_nat a n - Rexp_nat y n))
[apply Rle_plus_l;left;autobatch
| cut (∀x,y.(S x ≤ y) = (x < y));[2: intros; reflexivity]
- applyS Rexp_nat_tech;
- [ unfold lt; change in H1 with (O < n);
- autobatch; (*applyS H1;*)
- | assumption;
- | elim daemon; ]]
- (*
+ (* 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]]*)
+ |(* 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
[apply (nat_lt_to_R_lt ?? H1);
|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 ⊢ (?%?);