fact: Fixpoint open_cells_decomposition_contact open_cells pt : option (seq cell * seq cell * 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 Some(c :: cc, lc, c') else Some([::], q, c) else None else None.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL