-lapply (Rlt_times_l ? ? (Rinv x * Rinv y) H1)
-[rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin;
+lapply (Rlt_times_l (Rinv x * Rinv y) ? ? H1)
+[ lapply (Rinv_Rtimes_l x);[2: intro; destruct H2; autobatch;]
+ lapply (Rinv_Rtimes_l y);[2: intro; destruct H2; autobatch;]
+ cut ((x \sup -1/y*x<x \sup -1/y*y) = (y^-1 < x ^-1));[2:autobatch
+(* end auto($Revision: 9716 $) proof: TIME=2.24 SIZE=100 DEPTH=100 *) ;]
+ rewrite < Hcut; assumption;
+ (*
+ rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin;