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