proposition: Lemma proper_card A B : A \proper B -> #|A| < #|B|.
proof: Proof. by case/andP=> sAB nsBA; rewrite ltn_neqAle !(subset_leqif_card sAB) andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)