proposition: Lemma hull_monotone X Y : X `<=` Y -> hull X `<=` hull Y.
proof: Proof. move=> H a [n [g [d [d0 d1 gX ae]]]]; exists n, g, d; split => //. by eapply subset_trans; first exact: gX. 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)