proposition: Lemma inh_chooseE (T : inhType) (x0 : T) : choose xpredT x0 = @inh T.
proof: Proof. rewrite /choose; case: insubP => //= [[x Px]] _ /= ->. by rewrite inh_xchooseE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools