proposition: Lemma subenv_sn e1 e2 : wf_num e1 -> wf_num e2 -> subenv e1 e2 -> sn e1 <= sn e2.
proof: Proof. move=> /wf_sn-> /wf_sn-> /and5P[/eqP<-] H _ _ _. by rewrite ltnS; apply/subset_leq_card/setUS. Qed.
imports: mathcomp(all_ssreflect) bigmin extra