proposition: Lemma encompass_correct (l : seq Plane) (p : Plane) : uniq l -> (3 <= size l)%N -> encompass (ccw (R:=R)) l l -> encompass oriented [:: p] 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.
proof: Proof. move: l p. have orientedW: forall a b c, encompass.is_left oriented a b c -> oriented a b c. move=>a b c /or3P[| |//] /eqP<-; rewrite /oriented. by rewrite 2!det_cyclique det_alternate. by rewrite det_cyclique det_alternate. have H3 a b c p : uniq [:: a; b; c] -> encompass (ccw (R:=R)) [:: a; b; c] [:: a; b; c] -> encompass oriented [::p] [:: a; b; c] -> exists t : 'I_3 -> R, (forall i, 0 <= t i)%R /\ (\sum_i t i = 1%:R) /\ p = \sum_i t i *: [:: a; b; c]`_i. rewrite/uniq !in_cons negb_or 2!in_nil 2!orbF=>/andP [/andP[/negPf ab /negPf ac] /andP[/negPf bc _]] /andP[/andP [_ /andP [h _]] _] /= /andP [/andP [/orientedW cap _]] /andP [/andP [/orientedW abp _]] /andP [/andP [/orientedW bcp _] _]. move: h; rewrite/encompass.is_left bc eq_sym ab =>/= cab. exists (fun i => [:: det c p b / det c a b; det c a p / det c a b; det p a b / det c a b]`_i); split. case; case; [| case; [| case=>//]]; move=>/= _; (apply mulr_ge0; [| by rewrite invr_ge0; apply ltW]). - by rewrite 2!det_cyclique. - by []. - by rewrite det_cyclique. move: cab; rewrite /ccw lt0r=>/andP[cab _]. split. by rewrite !big_ord_recr big_ord0 /= add0r -2!mulrDl addrC addrA -decompose_det divff. rewrite !big_ord_recr big_ord0 /= add0r. apply (scalerI cab). rewrite 2!scalerDr 3!scalerA 3!mulrA 3![det c a b * _]mulrC -3!mulrA divff// 3!mulr1. apply/pair_eqP; apply/andP; split; apply/eqP; rewrite !develop_det /xcoord /ycoord; cbn; ring. move=> l p. elim: l=>// a; case=>// b; case=>// c; case. by move=>IHl abc _; apply H3. move=>d l IHl lu sl ll lp. case labp: (oriented b (last d l) p). move:H3=>/(_ a b (last d l) p); case. - move: lu; apply subseq_uniq=>/=. by rewrite eq_refl eq_refl -/(subseq [:: last d l] (c :: d :: l)) sub1seq in_cons mem_last orbT. - apply (Spec.encompassll_subseq lu)=>//. by rewrite /= eq_refl /= eq_refl -/(subseq [:: last d l] (c :: d :: l)) sub1seq in_cons mem_last orbT. - apply/andP; split. by move:lp=>/andP[lp _]; move:lp. apply/andP; split. by move:lp=>/andP[_ /andP[ap _]]. by rewrite /=/encompass.is_left labp !orbT. move=>f [f0 [f1 fp]]. exists (fun i:'I_(size l).+4 => (i == ord0)%:R * f ord0 + (i == lift ord0 ord0)%:R * f (lift ord0 ord0) + (i == ord_max)%:R * f ord_max). split. move=>i. apply addr_ge0; [apply addr_ge0|]; apply mulr_ge0; try apply f0; apply ler0n. split; rewrite big_ord_recr /= eq_refl mul1r 2!mul0r 2!add0r big_ord_recl /= mul1r 2!mul0r 2!addr0 big_ord_recl /= mul1r 2!mul0r addr0 add0r. rewrite -f1 ![\sum_i f _]big_ord_recl big_ord0 addr0 -!addrA; congr (_ + (_ + _)). rewrite -[f (lift _ (lift _ _))]add0r; congr (_ + f _); last by apply val_inj. rewrite -{3}(mul0r (\sum_(i < (size l).+1) 0)) mulr_sumr. apply congr_big=>// [[i ilt]] _. have ->: (widen_ord (leqnSn (size l).+3) (lift ord0 (lift ord0 (Ordinal ilt))) == ord_max) = false. by apply /negP=>/eqP/(f_equal val)/=; rewrite /bump/= 2!add1n=>/eqP; rewrite 2!eqSS=>/eqP ile; move:ilt; rewrite -ile ltnn. by rewrite 3!mul0r 2!addr0. rewrite fp ![\sum_i f _ *: _]big_ord_recl big_ord0 addr0 -!addrA; congr (_ + (_ + _)). rewrite (nth_last _ (d :: l))/= -[f (lift _ (lift _ _)) *: _]add0r; congr (_ + f _ *: _); last by apply val_inj. rewrite -{1}(scale0r (\sum_(i < (size l).+1) 0)) scaler_sumr. apply congr_big=>// [[i ilt]] _. have ->: (widen_ord (leqnSn (size l).+3) (lift ord0 (lift ord0 (Ordinal ilt))) == ord_max) = false. by apply /negP=>/eqP/(f_equal val)/=; rewrite /bump/= 2!add1n=>/eqP; rewrite 2!eqSS=>/eqP ile; move:ilt; rewrite -ile ltnn. by rewrite 2!mul0r 2!addr0 2!scale0r. case: IHl. - by move: lu=>/andP[_ lu]. - by []. - move: ll=>/Spec.encompassll_subseq; apply=>//; apply subseq_cons. - apply/andP; split. 2: by move: lp=>/andP[_ /andP [_ lp]]. rewrite/= andbT; apply/or3P/Or33. by rewrite/oriented det_inverse 2!det_cyclique leNgt oppr_lt0; apply/negP=>/ltW; move: labp; rewrite /oriented=>->. move=>f [f0 [f1 fp]]. exists (fun i=> match ord_S_split i with | inleft j => f (proj1_sig j) | inright _ => 0%:R end). split. by move=>i; case: (ord_S_split i). split; rewrite big_ord_recl; (case (ord_S_split ord0); [ by move=>[j H] | move=>_]); [| rewrite scale0r]; rewrite add0r. rewrite -f1; apply congr_big=>// [[i ilt]] _. case (ord_S_split _)=>// [[j jlt]] /=; congr (f _); apply val_inj=>/=. by move:jlt=>/(f_equal val)=>/=/eqP; rewrite /bump/= 2!add1n eqSS=>/eqP. rewrite fp; apply congr_big=>// [[i ilt]] _. case (ord_S_split _)=>// [[j jlt]] /=; congr (f _ *: _); apply val_inj=>/=. by move:jlt=>/(f_equal val)=>/=/eqP; rewrite /bump/= 2!add1n eqSS=>/eqP. 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)