proposition: Lemma unlift_none n (h : 'I_n) : unlift h h = None.
proof: Proof. by case: unliftP => // j Dh; case/eqP: (neq_lift h j). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)