proposition: Lemma gtree_mem0_cons_pairs 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 sub0 pt := gtree_pair_sub pt false in let t := GtreeNode t0 t1 t2 t3 in let t' := GtreeNode (sub0 pt0) (sub0 pt1) (sub0 pt2) (sub0 pt3) in gtree_mem (sub0 (gtree_cons_pairs t pt0 pt1 pt2 pt3)) =1 gtree_mem t'.
proof: Proof. move: pt0 pt1 pt2 pt3 => /= [t'0 t''0] [t'1 t''1] [t'2 t''2] [t'3 t''3]. rewrite /gtree_cons_pairs; case: gtree_empty4P => [[] * [|[] []] // | _]. case: gtree_empty4P => [[] | ] //= ppt0 ppt1 ppt2 ppt3 [|[] w] //=. - by case: gtree_mem (ppt0 w); case: gtree_mem; case: w. - by case: gtree_mem (ppt1 w); case: gtree_mem; case: w. - by case: gtree_mem (ppt2 w); case: gtree_mem; case: w. - by case: gtree_mem (ppt3 w); case: gtree_mem; case: w. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)