proposition: Lemma all_cells_have_left_neighbor : forallb (fun edge_list => let cells := edges_to_cells example_bottom example_top edge_list in forallb (fun c => (implb (andb (negb (Qeq_bool (left_limit c) (p_x (head dummy_pt (leftmost_points example_bottom example_top))))) (Nat.ltb 1 (List.length (left_pts c)))) (existsb (fun c' => lr_connected c' c) cells))) cells) example_edge_sets = true.
proof: Proof. easy. Qed.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL