proposition: Lemma subset_hull X : X `<=` hull X.
proof: Proof. move=> x xX; rewrite /hull; exists 1%N, (fun=> x), (fun=>1%R). split=> //; first by move=>_; exact ler01. - by rewrite big_ord_recl big_ord0 addr0. - by move=> d [i _ <-]. - by rewrite big_ord_recl big_ord0 scale1r addr0. 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)