fact: Definition complete_last_open (bottom top : edge) (c : cell) := match c with | Bcell lpts rpts le he => Bcell lpts (rightmost_points bottom top) le he end.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL