- generalize in match Hs;
- rewrite > (?:s = O);
- [2: cases Hs; lapply (os_le_to_nat_le ?? H1);
- apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin).
- |1: intros; lapply (os_le_to_nat_le (\fst (a O)) O (H2 O));
- lapply (le_n_O_to_eq ? Hletin); assumption;]
- |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n];
- apply (trans_le ??? (os_le_to_nat_le ?? H1));
+ generalize in match Hx;
+ 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).
+ |1: intros; unfold Type_of_ordered_set in sg;
+ 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);]
+ |2: right; cases Hx; rewrite > (sym_plus x O); split; [apply le_S_S; apply le_O_n];
+ apply (trans_le ??? (os_le_to_nat_le ?? H3));