proposition: Lemma gtree_mem_init_tree h w : gtree_mem (gtree_init_tree h) w = init_gtree_spec h w.
proof: Proof. case: h => [|h /=]; first by rewrite gtree_mem_empty; case: w. transitivity (gtree_mem (gtsub (gtree_init_table 0 h) 0 false) w). by case: (gtree_init_table 0 h). rewrite /init_gtree_spec; move: 0 {-2 3}0 false w (leqnn 0) => d. apply: (@proj2 ((d != 0) < size (gtree_init_table d h))). elim: h d => [|h IHh] d /=. by split=> [| [|[|[|n]]] [] [|s1 [|s2 w]] //]; by [case s1 | case d]. case: (gtree_init_table _ h) {IHh}(IHh d.+1) => [|pt1 [|pt0 lpt]] [_ Dsub] //. split=> [|dw bw w ledwd]; first by case: d lpt {Dsub} => [|[|d]] []. transitivity (gtree_mem (let elt := [:: empty_gtree_pair, pt1, pt0 & lpt] in GtreeNode (gtsub elt dw.+2 bw) (gtsub elt dw.+1 (~~ bw)) (gtsub elt dw bw) (gtsub elt dw (~~ bw))) w). elim: dw d ledwd pt0 pt1 empty_gtree_pair lpt {Dsub}. by case: bw => [] [|d] _ [t0 t0'] [t1 t1'] [t2 t3]. move=> dw IHdw [|d] ledwd // pt0 pt1 pt2 [{IHdw ledwd}|pt]; last exact: IHdw. case: dw => [|dw]; first by case: bw pt0 pt1 => [] [t1 t1'] [t2 t3]. case: dw => [|dw]; first by case: bw pt0 => [] [t2 t3]. by case: bw w => [] [|[] w]; rewrite /= ?gtree_mem_empty. have ledwd1 := leqW ledwd. case: w => [|[] w] //=; first 1 [exact: (Dsub dw.+1) | exact: Dsub]; by case: dw {ledwd ledwd1}(leqW ledwd1) => [|dw]; last exact: Dsub; case: bw; rewrite andbF /= gtree_mem_empty. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree dyck)