proposition: Lemma lt_def s1 s2 : lt s1 s2 = (s2 != s1) && le s1 s2.
proof: Proof. elim: s1 s2 => [|x s1 ihs1] [|y s2]//=. by rewrite eqseq_cons ihs1; case: comparableP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)