proposition: Fact lex1 (x : {t : T & T' t}) : x <= Tagged T' (\top : T' \top).
proof: Proof. rewrite leEsig /=; case: comparableP (lex1 (tag x)) => //=. by case: x => //= x px x0; rewrite x0 in px *; rewrite tagged_asE lex1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)