proposition: Lemma encompassP (l : seq Plane) (p : Plane) : uniq l -> (3 <= size l)%N -> encompass (ccw (R:=R)) l l -> reflect (p \in hull (fun x => x \in l)) (encompass oriented [:: p] l).
proof: Proof. move=>lu ls ll; apply/(iffP idP). move=>/(encompass_correct lu ls ll)[f [f0 [f1 ->]]]. rewrite inE/hull/=; exists (size l), (fun i=> l`_i), f; split => //. by move =>// x/= [i] _ <-{x}; exact: (@mem_nth Plane). rewrite inE/hull/= =>[[n [g [d [d0 d1 gl pe]]]]]. apply encompass_complete=>//. exists (fun i=> \sum_(j < n | g j == l`_i) d j); split. by move=>i; apply sumr_ge0. split. rewrite -(big_map (fun i: 'I_(size l) => l`_i) xpredT (fun x=> \sum_(j < n | g j == x) d j)). rewrite (map_comp (fun i : nat => l`_i) (@nat_of_ord (size l))). move:(val_enum_ord (size l)); rewrite enumT=>->. rewrite map_nth_iota0// take_size -big_partition//. by apply/allP=>i _; apply gl. transitivity (\sum_(i < size l) \sum_(j < n | g j == l`_i) d j *: g j). rewrite -(big_map (fun i: 'I_(size l) => l`_i) xpredT (fun x=> \sum_(j < n | g j == x) d j *: g j)). rewrite (map_comp (fun i : nat => l`_i) (@nat_of_ord (size l))). move:(val_enum_ord (size l)); rewrite enumT=>->. rewrite map_nth_iota0// take_size -big_partition//. by apply/allP=>i _; apply gl. apply congr_big=>//i _. rewrite scaler_suml. by apply congr_big=>//j/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)