fact: Fixpoint open_cells_decomposition_rec open_cells pt : seq cell * seq cell * cell * seq cell := if open_cells is c :: q then if contains_point pt c then if open_cells_decomposition_contact q pt is Some(cc, lc, c') then ([::], c :: cc, c', lc) else ([::], [::], c, q) else let '(fc, cc, c', lc) := open_cells_decomposition_rec q pt in (c :: fc, cc, c', lc) else ([::], [::], dummy_cell, [::]).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL