fact: Definition decode (x : GenTree.tree R) : option (\bar R) := match x with | GenTree.Node 0 [:: GenTree.Leaf r] => Some r%:E | GenTree.Node 1 [::] => Some +oo | GenTree.Node 2 [::] => Some -oo | _ => None end.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed