proposition: Lemma sub_num_lt e1 e2 : subenv e1 e2 -> forall x, (num e1 x < sn e1) = (num e2 x < sn e1).
proof: Proof. move=> /and3P[_ /forall_inP /(_ _ _)/eqP num_eq /forall_inP] num_lt x. have nume1_lt := num_lt x; apply/idP/idP => // {}nume1_lt. by rewrite num_eq ?inE// (leq_trans (ltnW nume1_lt))// max_card. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors