proposition: Lemma set_lt_Cantor M N: nonempty M -> (M <s N <-> ( (exists N1, [/\ sub N1 N, nonempty N1 & N1 \Eq M]) /\ ~ (exists M1, [/\ sub M1 M, nonempty M1 & M1 \Eq N]))).
proof: Proof. move => neM. split. move =>[ h ne]; split. move/set_leP: h =>[M1 qa /EqS qb]; exists M1; split => //. apply/nonemptyP => me1. move:(EqS qb) => [g [bg sg tg]]. case:neM => y; rewrite - sg => ysg. by move:(Vf_target (proj1(proj1 bg)) ysg); rewrite tg me1 => /in_set0. move => [M1 [qa qb /EqS qc]]. have h2: N <=s M by apply/set_leP;exists M1. by case: ne; apply: set_leA. move => [ [N1 [N1N _ /EqS p1]] p2]. split; first by apply/set_leP; exists N1. move => eq1; case: p2; exists M; split => //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)