fact: Fixpoint flatq q : seq nat := match q with | Qask0 => [::] | Qask1 qa => [:: qa : nat] | QaskL qa ql => (qa : nat) :: flatq ql | QaskR qa qr => (qa : nat) :: flatq qr | QaskLR qa ql qr => (qa : nat) :: flatq ql ++ flatq qr | QaskLL qa qll => (qa : nat) :: flatq qll | QaskRR qa qrr => (qa : nat) :: flatq qrr end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry coloring)