proposition: Lemma subgrectE x0 x1 x2 x3 y0 y1 y2 y3 : [/\ x0 <= x1, x2 <= x3, y0 <= y1 & y2 <= y3] -> subpred (Grect x1 x2 y1 y2) (Grect x0 x3 y0 y3).
proof: Proof. case=> lex01 lex23 ley01 ley23 [x y] /andP[] /=. by do 2![case/andP=> /(le_trans _)-> // /lt_le_trans-> //]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)