proposition: Lemma setP_S a b: sub a b <-> sub (\Po a) (\Po b).
proof: Proof. split => sab. move=> x /setP_P sxa; apply /setP_P; apply: (sub_trans sxa sab). by apply /setP_P;apply: sab; apply /setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)