fact: Definition encompass (s h : seq plane) := match h with | nil => false | t :: h' => encompass_aux s (last t h' :: h) end.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets) mathcomp(zmodp) preliminaries preliminaries_hull axiomsKnuth