proposition: Lemma encompassE (s h : seq plane) : encompass s h = (h != [::]) && all (fun x => encompass [:: x] h) s.
proof: Proof. by case: h =>// a l; rewrite {1}/encompass encompass_auxE. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets) mathcomp(zmodp) preliminaries preliminaries_hull axiomsKnuth