proposition: Lemma itv_bound_can : cancel (fun b : itv_bound T => match b with BSide b x => (b, Some x) | BInfty b => (b, None) end) (fun b => match b with (b, Some x) => BSide b x | (b, None) => BInfty _ b end).
proof: Proof. by case. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)