proposition: Lemma Exercise4_6c: exists h, E46_hp h.
proof: Proof. have hm: E46_hprop m. move=> r Z le1 Zd cT. exists emptyset;split;fprops;last by move=> j /in_set0. rewrite (cdiff_nn m) in le1. rewrite (cle0 le1) cardinal_set0 //. move: (least_int_prop (p:= E46_hprop) mN hm). set y := (least_ordinal E46_hprop m); move => [yN hy yl]. exists y; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)