proposition: Lemma encompass_all_index (l s : seq plane) : encompass s l = (l != [::]) && [forall i : 'I_(size l), all_left l`_i l`_i.+1mod s].
proof: Proof. case: l => // a l /=. rewrite -/(encompass_aux s (a :: l)) encompass_aux_all_index. apply/idP/idP => [H|/forallP H]. apply/forallP => -[i ilt]. move: ilt (ilt); rewrite {1}ltnS leq_eqVlt => /predU1P[-> /= _|ilt ilt1]. by rewrite modnn nth_last /=; move: H => /andP[H _]. move: H => /andP[_ /andP [_ /forallP]] /(_ (Ordinal ilt1)) /=. by rewrite modn_small ?ltnS. apply/andP; split. by move: H => /(_ ord_max); rewrite /= modnn nth_last. apply/forallP => -[i ilt]. move: ilt (ilt); rewrite {1}ltnS leq_eqVlt => /predU1P[-> /= _|ilt ilt1]. by rewrite modnn. by move: H => /(_ (Ordinal ilt1))/=; rewrite modn_small ?ltnS. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets) mathcomp(zmodp) preliminaries preliminaries_hull axiomsKnuth