proposition: Lemma ord_S_split n (i: 'I_n.+1): {j: 'I_n | i = lift ord0 j} + {i = ord0}.
proof: Proof. case: i; case=>[| i] ilt. by right; apply val_inj. by left; exists (Ordinal (ltnSE ilt)); apply val_inj. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)