proposition: Lemma sub_trans : transitive subenv.
proof: Proof. move=> e2 e1 e3 sub12 sub23; rewrite /subenv. rewrite (subset_trans (sub_sccs sub12))// ?sub_sccs//=. apply/andP; split; apply/forall_inP=> x xP. by rewrite (sub_snum sub23) ?(sub_snum sub12)//. have x2 : num e3 x < sn e2 by rewrite (leq_trans xP)// leq_sn. by rewrite (sub_num_lt sub12)// -(sub_vnum sub23)// (sub_num_lt sub23). Qed.
imports: mathcomp(all_ssreflect) extra_nocolors