proposition: Lemma properEcard A B : (A \proper B) = (A \subset B) && (#|A| < #|B|).
proof: Proof. by rewrite properEneq ltnNge andbC eqEcard; case: (A \subset B). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)