proposition: Lemma encompass_auxE (l h : seq plane) : encompass_aux l h = (h != [::]) && all (fun x => encompass_aux [:: x] h) l.
proof: Proof. elim: h =>// a'; case=> [ _ | b' l' IHl']. by elim: l. rewrite /= -/(encompass_aux l (b' :: l')) IHl' -all_predI; apply eq_all=>x. by rewrite /= andbT. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets) mathcomp(zmodp) preliminaries preliminaries_hull axiomsKnuth