proposition: Lemma allLtn_notin s b : allLeq s b -> b \notin s -> allLtn s b.
proof: Proof. Proof using. elim: s => //= s0 s IHs /andP[]. rewrite lt_neqAle => -> {}/IHs Hrec. by rewrite inE negb_or eq_sym => /andP[->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools