proposition: Lemma di_eq2 {i x} : x ≥ i → di i x = S x.
proof: Proof. intros lt. unfold di. induction (natlthorgeh x i) as [P|_]. - apply fromempty. exact (natlthtonegnatgeh _ _ P lt). - apply idpath. Defined.
imports: UniMath.Foundations.Sets