proposition: Lemma gtree_cons_pairs_partition t0 t1 t2 t3 pt0 pt1 pt2 pt3 : gtree_pair_partition t0 pt0 -> gtree_pair_partition t1 pt1 -> gtree_pair_partition t2 pt2 -> gtree_pair_partition t3 pt3 -> let t := GtreeNode t0 t1 t2 t3 in gtree_pair_partition t (gtree_cons_pairs t pt0 pt1 pt2 pt3).
proof: Proof. case: pt0 pt1 pt2 pt3 => [t'0 t''0] [t'1 t''1] [t'2 t''2] [t'3 t''3] *. rewrite /gtree_cons_pairs. do 2![case: gtree_empty4P => [[] w| _]; first by rewrite gtree_mem_empty; case: ifP]. by case=> [|[]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)