rewrite > (?:x = O);
[2: cases Hx; lapply (os_le_to_nat_le ?? H1);
apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin).
rewrite > (?:x = O);
[2: cases Hx; lapply (os_le_to_nat_le ?? H1);
apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin).
lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P;
simplify in P:(???%); lapply (le_transitive ??? P H1) as W;
lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);]
lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P;
simplify in P:(???%); lapply (le_transitive ??? P H1) as W;
lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);]