proposition: Lemma PCanHasChoice f' : pcancel f f' -> hasChoice sT.
proof: Proof. move=> fK; pose liftP sP := [pred x | oapp sP false (f' x)]. pose sf sP := [fun n => obind f' (find (liftP sP) n)]. exists sf => [sP n x | sP [y sPy] | sP sQ eqPQ n] /=. - by case Df: (find _ n) => //= [?] Dx; have:= correct Df; rewrite /= Dx. - have [|n Pn] := @complete T (liftP sP); first by exists (f y); rewrite /= fK. exists n; case Df: (find _ n) Pn => //= [x] _. by have:= correct Df => /=; case: (f' x). by congr (obind _ _); apply: extensional => x /=; case: (f' x) => /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)