proposition: Lemma encompass_complete (l : seq Plane) (p : Plane) : uniq l -> (3 <= size l)%N -> encompass (ccw (R:=R)) l l -> (exists t : 'I_(size l) -> R, (forall i, 0 <= t i)%R /\ (\sum_i t i = 1%:R) /\ p = \sum_i t i *: l`_i) -> encompass oriented [:: p] l.
proof: Proof. move=>lu ls ll [f [f0 [f1 fp]]]; subst p. rewrite encompass_all_index; apply/andP; split. by case: l lu ls ll f f0 f1. apply/forallP=>[[i ilt]]. rewrite/= andbT is_left_oriented /oriented. wlog: l lu ls ll f f0 f1 i ilt / l`_i == 0%R. move=>h. set l' := [seq x - l`_i | x <- l]. have subl': forall a b, (a < size l) -> (b < size l) -> l'`_a - l'`_b = l`_a - l`_b. by move=>a b al bl; rewrite (nth_map (GRing.zero _))// (nth_map (GRing.zero _))// opprD [-_ - - _]addrC -!addrA; congr GRing.add; rewrite addrA subrr add0r. suff: (0%:R <= det l'`_i l'`_(Zp_succ (Ordinal ilt)) (\sum_(i0 < size l) f i0 *: l'`_i0))%R. congr (_ <= _)%R; rewrite 2!det_scalar_productE; congr (scalar_product _ (rotate _)). - by apply subl'=>//; case: (Zp_succ (Ordinal ilt)). - rewrite [l'`_i](nth_map (GRing.zero _))// subrr subr0 -[l`_i]scale1r. have->: (1 = 1%:R)%R by []. rewrite -f1 scaler_suml -sumrB; apply congr_big=>// [[j jlt]] _. by rewrite -scalerBr (nth_map (GRing.zero _)). move:h=>/(_ l'); rewrite size_map; apply. - rewrite map_inj_uniq=>//; apply addIr. - by []. - rewrite Spec.encompassll_spec. 2: by rewrite map_inj_uniq=>//; apply addIr. apply/andP; split. by destruct l. rewrite size_map. apply/forallP=>[[a alt]]. apply/forallP=>[[b blt]]. apply/forallP=>[[c clt]]. apply/implyP=>abc. rewrite /ccw_KA.OT /ccw det_scalar_productE subl'// subl'//. by move:ll; rewrite Spec.encompassll_spec=>// /andP[_] /forallP /(_ (Ordinal alt)) /forallP /(_ (Ordinal blt)) /forallP /(_ (Ordinal clt)) /implyP /(_ abc); rewrite /ccw_KA.OT /ccw det_scalar_productE. - apply f0. - exact f1. - by rewrite (nth_map (GRing.zero _))// subrr. move=>/eqP li0; rewrite li0 det_sum; apply sumr_ge0=>[[j jlt]] _. rewrite det_scalar_productE 2!subr0 rotateZ scalar_productZR; apply mulr_ge0. apply f0. move:ll; rewrite encompassE =>/andP[_ /allP ll]. have/ll: l`_(Ordinal jlt) \in l by rewrite mem_nth. rewrite encompass_all_index=>/andP[_] /forallP /(_ (Ordinal ilt))/=; rewrite andbT. rewrite li0// => /or3P[/eqP ->|/eqP ->|]. - by rewrite -{2}(scale0r 0) rotateZ scalar_productZR mul0r. - by rewrite scalar_product_rotatexx. - by rewrite /ccw det_scalar_productE 2!subr0=>/ltW. Qed.
imports: encompass conv mathcomp(all_ssreflect all_algebra vector reals normedtype) mathcomp(classical_sets boolp mathcomp_extra) counterclockwise mathcomp.algebra_tactics(ring) mathcomp.zify(zify)