-definition sd_O: ∀h. sd h ≝ λh. mk_sd h deg_O ….
-/2 width=2 by le_n_O_to_eq, le_n, ex_intro/ defined.
-
-(* Basic_2A1: includes: deg_SO_pos *)
-inductive deg_SO (h:sh) (s:nat) (s0:nat): predicate nat ≝
-| deg_SO_succ : ∀n. (next h)^n s0 = s → deg_SO h s s0 (↑n)
-| deg_SO_zero: ((∃n. (next h)^n s0 = s) → ⊥) → deg_SO h s s0 0
-.
-
-fact deg_SO_inv_succ_aux: ∀h,s,s0,n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n →
- (next h)^n s0 = s.
-#h #s #s0 #n0 * -n0
-[ #n #Hn #x #H destruct //
-| #_ #x #H destruct
-]
-qed-.
-
-(* Basic_2A1: was: deg_SO_inv_pos *)
-lemma deg_SO_inv_succ: ∀h,s,s0,n. deg_SO h s s0 (↑n) → (next h)^n s0 = s.
-/2 width=3 by deg_SO_inv_succ_aux/ qed-.
-
-lemma deg_SO_refl: ∀h,s. deg_SO h s s 1.
-#h #s @(deg_SO_succ … 0 ?) //
-qed.
-
-lemma deg_SO_gt: ∀h,s1,s2. s1 < s2 → deg_SO h s1 s2 0.
-#h #s1 #s2 #HK12 @deg_SO_zero * #n elim n -n normalize
-[ #H destruct
- elim (lt_refl_false … HK12)
-| #n #_ #H
- lapply (next_lt h ((next h)^n s2)) >H -H #H
- lapply (transitive_lt … H HK12) -s1 #H1
- lapply (nexts_le h s2 n) #H2
- lapply (le_to_lt_to_lt … H2 H1) -h -n #H
- elim (lt_refl_false … H)
-]
-qed.
-
-definition sd_SO: ∀h. nat → sd h ≝ λh,s. mk_sd h (deg_SO h s) ….
-[ #s0
- lapply (nexts_dec h s0 s) *
- [ * /3 width=2 by deg_SO_succ, ex_intro/ | /4 width=2 by deg_SO_zero, ex_intro/ ]
-| #K0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2 //
- [ < H2 in H1; -H2 #H
- lapply (nexts_inj … H) -H #H destruct //
- | elim H1 /2 width=2 by ex_intro/
- | elim H2 /2 width=2 by ex_intro/
- ]
-| #s0 #n *
- [ #d #H destruct elim d -d normalize
- /2 width=1 by deg_SO_gt, deg_SO_succ, next_lt/
- | #H1 @deg_SO_zero * #d #H2 destruct
- @H1 -H1 @(ex_intro … (↑d)) /2 width=1 by sym_eq/ (**) (* explicit constructor *)
- ]
-]
-defined.