proposition: Lemma get_mk_ord n x: get_ord n (mk_ord x) = Some x.
proof: Proof. unfold mk_ord, get_ord. destruct x as [i Hi]; simpl. rewrite get_mk_nat. case lt_ge_dec. intro. f_equal. now apply eq_ord. rewrite Hi at 1. discriminate. Qed.
imports: common positives ordinal