proposition: Lemma enumerableI {X Y: Type} {enum: Enumerable X} (to_X: Y -> X) (of_X: X -> Y) : (forall (y: Y), of_X (to_X y) = y) -> Enumerable Y.
proof: Proof. move=> cancel. exists (fun y => to_nat (to_X y)) (fun x => of_X (of_nat x)). move=> y. by rewrite enumP cancel. Qed.
imports: ssreflect ssrbool ssrfun