+nlet rec iso_nat_nat_union (s: nat → nat) m index on index : pair nat nat ≝
+ match ltb m (s index) with
+ [ true ⇒ mk_pair … index m
+ | false ⇒
+ match index with
+ [ O ⇒ (* dummy value: it could be an elim False: *) mk_pair … O O
+ | S index' ⇒ iso_nat_nat_union s (minus m (s index)) index']].
+
+alias symbol "eq" = "leibnitz's equality".
+naxiom plus_n_O: ∀n. plus n O = n.
+naxiom ltb_t: ∀n,m. n < m → ltb n m = true.
+naxiom ltb_f: ∀n,m. ¬ (n < m) → ltb n m = false.
+naxiom ltb_cases: ∀n,m. (n < m ∧ ltb n m = true) ∨ (¬ (n < m) ∧ ltb n m = false).
+naxiom minus_canc: ∀n. minus n n = O.
+naxiom ad_hoc9: ∀a,b,c. a < b + c → a - b < c.
+naxiom ad_hoc10: ∀a,b,c. a - b = c → a = b + c.
+naxiom ad_hoc11: ∀a,b. a - b ≤ S a - b.
+naxiom ad_hoc12: ∀a,b. b ≤ a → S a - b - (a - b) = S O.
+naxiom ad_hoc13: ∀a,b. b ≤ a → (O + (a - b)) + b = a.
+naxiom ad_hoc14: ∀a,b,c,d,e. c ≤ a → a - c = b + d + e → a = b + (c + d) + e.
+naxiom not_lt_to_le: ∀a,b. ¬ (a < b) → b ≤ a.
+naxiom split_big_plus:
+ ∀n,m,f. m ≤ n →
+ big_plus n f = big_plus m (λi,p.f i ?) + big_plus (n - m) (λi.λp.f (i + m) ?).
+ nelim daemon.
+nqed.
+
+ntheorem iso_nat_nat_union_char:
+ ∀n:nat. ∀s: nat → nat. ∀m:nat. m < big_plus (S n) (λi.λ_.s i) →
+ let p ≝ iso_nat_nat_union s m n in
+ m = big_plus (n - fst … p) (λi.λ_.s (S (i + fst … p))) + snd … p ∧
+ fst … p ≤ n ∧ snd … p < s (fst … p).
+ #n; #s; nelim n
+ [ #m; nwhd in ⊢ (??% → let p ≝ % in ?); nwhd in ⊢ (??(??%) → ?);
+ nrewrite > (plus_n_O (s O)); #H; nrewrite > (ltb_t … H); nnormalize;
+ napply conj [ napply conj [ napply refl | napply le_n ] ##| nassumption ]
+##| #n'; #Hrec; #m; nwhd in ⊢ (??% → let p ≝ % in ?); #H;
+ ncases (ltb_cases m (s (S n'))); *; #H1; #H2; nrewrite > H2;
+ nwhd in ⊢ (let p ≝ % in ?); nwhd
+ [ napply conj [napply conj
+ [ nwhd in ⊢ (????(?(?%(λ_.λ_:(??%).?))%)); nrewrite > (minus_canc n'); napply refl
+ | nnormalize; napply le_n]
+ ##| nnormalize; nassumption ]
+ ##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i));
+ ngeneralize in match (Hrec (m - s (S n')) ?) in ⊢ ?
+ [##2: napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; napply conj
+ [##2: nassumption
+ |napply conj
+ [napply (eq_rect_CProp0_r ?? (λx.λ_. m = x + snd … (iso_nat_nat_union s (m - s (S n')) n')) ??
+ (split_big_plus
+ (S n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
+ (n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
+ (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n'))))?))
+ [##2: napply ad_hoc11]
+ napply (eq_rect_CProp0_r ?? (λx.λ_. ? = ? + big_plus x (λ_.λ_:? < x.?) + ?)
+ ?? (ad_hoc12 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?))
+ [##2: nassumption]
+ nwhd in ⊢ (???(?(??%)?));
+ nrewrite > (ad_hoc13 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?)
+ [##2: nassumption]
+ napply ad_hoc14 [ napply not_lt_to_le; nassumption ]
+ nwhd in ⊢ (???(?(??%)?));
+ napply (eq_rect_CProp0_r ?? (λx.λ_. ? = x + ?) ??
+ (plus_n_O (big_plus (n' - fst … (iso_nat_nat_union s (m - s (S n')) n'))
+ (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n')))))));
+ nassumption
+ | napply le_S; nassumption ]##]##]##]
+nqed.
+
+