proposition: Lemma subitv_trans : transitive subitv.
proof: Proof. case=> [yl yr][xl xr][zl zr] /andP [Hl Hr] /andP [Hl' Hr'] /=. by rewrite (le_trans Hl' Hl) (le_trans Hr Hr'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)