proposition: Lemma encompassll_subseq (l l' : seq plane) : uniq l -> encompass oriented l l -> subseq l' l -> l' != [::] -> encompass oriented l' l'.
proof: Proof. move=> lu; rewrite (encompassll_spec lu) => ll l'l l'0. have l'u := subseq_uniq l'l lu; rewrite (encompassll_spec l'u) l'0 /=. apply/'forall_'forall_'forall_implyP => i j k /andP[ij jk]. move: l'l => /subseq_incl-/(_ 0%R) [f [fl flt]]. move: ll => /andP[_] /'forall_'forall_'forall_implyP /(_ (f i)) /(_ (f j)) /(_ (f k)); rewrite 3!fl; apply. by apply/andP; split; apply: flt. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets) mathcomp(zmodp) preliminaries preliminaries_hull axiomsKnuth