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]
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]