proposition: Lemma etp_bij A B f: inc f (bijections A B) -> inc (\Pof f) (bijections (\Po A) (\Po B)).
proof: Proof. move /bijectionsP => [bf sd tf]. have: inc f (functions A B) by apply/functionsP; split => //; fct_tac. move /etp_fun =>/functionsP [_ sf' st']. apply/bijectionsP; split => //. split;[ apply: (etp_fi (proj1 bf)) | apply: (etp_fs (proj2 bf))]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)