proposition: Lemma proper_size X Y : X `<` Y -> size X < size Y.
proof: Proof. rewrite properEneq ltn_neqAle => /andP [H1 H2]. rewrite subset_size // andbT eqn_leq. apply/negP => /andP [_ H]. by rewrite (subsize_eq H2 H) eqxx in H1. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)