proposition: Lemma encompass_aux_all_index (l h : seq plane) : encompass_aux l h = (h != [::]) && [forall i : 'I_(size h), (i.+1mod == 0%N :> nat) || all_left h`_i h`_i.+1mod l].
proof: Proof. elim: h=>// a; case. by move=>/= _; apply/esym/forallP => i; rewrite modn1 eq_refl. move=>b l' IHl' /=; rewrite -/(encompass_aux l (b :: l')) IHl' /=. apply/idP/idP => [/andP[Habl H]|/forallP H]. apply/forallP => -[] [//|n/=]. rewrite ltnS => nlt. move: H => /forallP/(_ (Ordinal nlt)). move: nlt (nlt); rewrite {1}ltnS leq_eqVlt => /predU1P[-> mm _|nm nm1]. by rewrite modnn eqxx. by rewrite modn_small ?ltnS// modn_small ?ltnS. apply/andP; split; first by move: H => /(_ ord0). apply/forallP => -[i ilt]. move: H => /(_ (lift ord0 (Ordinal ilt))). move: ilt (ilt); rewrite {1}ltnS leq_eqVlt => /predU1P[-> mm _|ilt ilt1]. by rewrite modnn eqxx. by rewrite modn_small ?ltnS// modn_small ?ltnS. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets) mathcomp(zmodp) preliminaries preliminaries_hull axiomsKnuth