+[ 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:
+ demodulate all;]
+ rewrite < Hcut; assumption;
+ (*
+ rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin;