proposition: Lemma example_inside_box : forallb (fun edge_list => forallb (fun e => inside_box (point e) example_bottom example_top) (edges_to_events edge_list)) example_edge_sets = true.
proof: Proof. easy. Qed.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL