proposition: Lemma hull0 : hull set0 = set0 :> set A.
proof: Proof. rewrite funeqE => d; rewrite propeqE; split => //. move=> [n [g [e [e0 e1 gX ->{d}]]]]. destruct n as [|n]; first by rewrite big_ord0 in e1; move:(@ltr01 R); rewrite e1 ltxx. exfalso; apply: (gX (g ord0)); exact/imageP. 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)