proposition: Lemma encompassll_spec (l : seq plane) : uniq l -> encompass oriented l l = (l != [::]) && [forall i : 'I_(size l), [forall j : 'I_(size l), [forall k : 'I_(size l), (i < j < k)%N ==> oriented l`_i l`_j l`_k]]].
proof: Proof. move=> /uniqP-/(_ 0%R) lu; apply/idP/idP. rewrite encompassE => /andP[-> /allP] ll /=. have sD i j : (i.+1 < size l)%N -> (j < size l)%N -> j != i -> j != i.+1 -> oriented l`_i l`_i.+1 l`_j. move=> isl jl ji jis. have /ll : l`_j \in l by rewrite mem_nth. have il : (i < size l)%N by rewrite (leq_trans _ isl). rewrite encompass_all_index => /andP[_] /forallP /(_ (Ordinal il)) /=. rewrite Zp_succE andbT/= modn_small// => /or3P[| |//] /eqP/lu; rewrite 2!inE. by move=> /(_ jl il)/eqP; rewrite (negbTE ji). by move=>/(_ jl isl)/eqP; rewrite (negbTE jis). apply/'forall_'forall_'forall_implyP => -[i ilt] [j jlt] [k klt] /= /andP[ij jk]. elim: k => // k IHk in klt jk *. have {}IHk := IHk (ltnW klt). move: jk; rewrite leq_eqVlt => /predU1P[[jk]|]. subst j. do 2 apply: Ax1. apply: sD => //; first by rewrite ltn_eqF. by rewrite ltn_eqF// (leq_trans ij). rewrite ltnS => jk; have {}IHk := IHk jk. move: ij; rewrite leq_eqVlt => /predU1P[ij|ij]. subst j. apply: sD => //. by rewrite gtn_eqF// ltnS (leq_trans _ jk)// -addn2 leq_addr. by rewrite gtn_eqF// (leq_trans jk). apply: (@Ax5 _ l`_i.+1 _ l`_k). - apply: sD => //; first by rewrite (leq_trans ij)// ltnW. by rewrite gtn_eqF// (ltn_trans _ ij). by rewrite gt_eqF. - apply: sD; first by rewrite (leq_trans ij)// ltnW. by rewrite (ltn_trans _ klt). by rewrite gtn_eqF// (ltn_trans _ jk)// (ltn_trans _ ij). by rewrite gtn_eqF// (ltn_trans ij). - apply: sD => //; first by rewrite (leq_trans ij)// ltnW. rewrite gtn_eqF// ltnS (leq_trans _ (ltnW jk))// (leq_trans _ ij)//. by rewrite -addn2 leq_addr. by rewrite gtn_eqF// (leq_trans ij)// (leq_trans (ltnW jk)). - exact IHk. - do 2 apply Ax1. apply: sD => //. by rewrite ltn_eqF// (ltn_trans _ jk)// (leq_trans _ ij). by rewrite ltn_eqF// ltnS (leq_trans _ (ltnW jk))// ltnW// (ltn_trans _ ij). rewrite encompassE => /andP[l0 sD] /=; rewrite l0 /=. have id x : x \in l -> exists2 n, (n < size l)%N & l`_n = x. by move=> xl; exists (index x l); [rewrite index_mem|rewrite nth_index]. apply/allP => _ /id[i il <-]. rewrite encompass_all_index; rewrite l0; apply/forallP => -[j jlt]. rewrite /all_left/= /is_left/= andbT. have [->|ij] := eqVneq i j. exact/or3P/Or31. destruct l as [|a l] => //=. have [ijs|ijs] := eqVneq i (j.+1 %% (size l).+1)%N. by apply/or3P/Or32; rewrite -ijs. apply/or3P/Or33; move: jlt; rewrite leq_eqVlt => /predU1P[[je]|jlt]. subst j; rewrite modnn. do 2 apply Ax1. move: sD => /'forall_'forall_'forall_implyP /(_ ord0 (Ordinal il) (Ordinal (leqnn _))); apply => /=. rewrite lt0n. move: ijs; rewrite modnn => ->/=. move: il; rewrite leq_eqVlt => /predU1P[[/eqP]|]. by rewrite (negbTE ij). by rewrite ltnS. move:ijs; rewrite modn_small => // ijs. have [ji|ji] := ltnP j.+1 i. move: sD => /'forall_'forall_'forall_implyP /(_ (Ordinal (leq_trans (leqnSn _) jlt)) (Ordinal jlt) (Ordinal il)). apply => /=. by rewrite ltnS leqnn. apply: Ax1. move: sD => /'forall_'forall_'forall_implyP /(_ (Ordinal il) (Ordinal (leq_trans (leqnSn _) jlt)) (Ordinal jlt)). apply => /=. rewrite ltnS leqnn andbT ltnNge. rewrite leq_eqVlt eq_sym (negbTE ij)/=. rewrite leq_eqVlt eq_sym (negbTE ijs)/=. by rewrite ltnNge ji. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets) mathcomp(zmodp) preliminaries preliminaries_hull axiomsKnuth