proposition: Lemma exercise5_f1 x y: sub (powerset x) (powerset y) -> sub x y.
proof: Proof. move=> sxy z zx. have p2: sub (singleton z) y. by apply /setP_P; apply: sxy; apply /setP_P => t /set1_P ->. apply: (p2 z); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)