(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Nat.ma: Natural numbers and common arithmetical functions.                 *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
include "Cartesian.ma".
include "Bool.ma".
include "Connectives.ma".

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* The datatype.                                                              *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
ninductive Nat: Type[0] ≝
  Z: Nat
| S: Nat → Nat.

ntheorem S_inj: ∀n,m:Nat. S n = S m → n=m.
 #n m H;
 nchange with (n = match S m with [ Z ⇒ Z | S x ⇒ x]);
 napply (match H return λx.λ_. n = match x with [Z ⇒ Z | S x ⇒ x] with [ refl ⇒ ? ]);
 nnormalize; /3/.
nqed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Orderings.                                                                 *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝
  ltoe_refl: less_than_or_equal_p n n
| ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m).

nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝
  match m with
    [ Z ⇒ true
    | S o ⇒
      match n with
        [ Z ⇒ false
        | S p ⇒ less_than_or_equal_b o p
        ]
    ].
    
notation "hvbox(n break ≤ m)"
  non associative with precedence 47
  for @{ 'less_than_or_equal $n $m }.
  
interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).

notation "hvbox(n break ≲ m)"
  non associative with precedence 47
  for @{ 'less_than_or_equalb $n $m }.

interpretation "Nat less than or equal bool" 'less_than_or_equalb n m = (less_than_or_equal_b n m).


ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
  λm, n: Nat.
    n ≤ m.

ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝
  λm, n: Nat.
    less_than_or_equal_b n m.
    
notation "hvbox(n break ≥ m)"
  non associative with precedence 47
  for @{ 'greater_than_or_equal $n $m }.
  

interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).

notation "hvbox(n break ≳ m)"
  non associative with precedence 47
  for @{ 'greater_than_or_equalb $n $m }.

interpretation "Nat greater than or equal bool" 'greater_than_or_equalb n m = (greater_than_or_equal_b n m).


(* Add Boolean versions.                                                      *)
ndefinition less_than_p ≝
  λm: Nat.
  λn: Nat.
    less_than_or_equal_p (S m) n.
    
notation "hvbox(n break < m)"
  non associative with precedence 47
  for @{ 'less_than $n $m }.
  
interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).

ndefinition greater_than_p ≝
  λm, n: Nat.
    n < m.
    
notation "hvbox(n break > m)"
  non associative with precedence 47
  for @{ 'greater_than $n $m }.
  
interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).

nlet rec less_than_b (m: Nat) (n: Nat) on m ≝
  match m with
    [ Z ⇒
      match n with
        [ Z ⇒ false
        | S o ⇒ true
        ]
    | S o ⇒
      match n with
        [ Z ⇒ false
        | S p ⇒ less_than_b o p
        ]
    ].

(* interpretation "Nat less than bool" 'less_than n m = (less_than_b n m). *)

ndefinition greater_than_b ≝
  λm, n: Nat.
    less_than_b n m.
    
(* interpretation "Nat greater than bool" 'greater_than n m = (greater_than_b n m). *)

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Addition and subtraction.                                                  *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
nlet rec plus (n: Nat) (o: Nat) on n ≝
  match n with
    [ Z ⇒ o
    | S p ⇒ S (plus p o)
    ].
    
notation "hvbox(n break + m)"
  right associative with precedence 52
  for @{ 'plus $n $m }.
  
interpretation "Nat plus" 'plus n m = (plus n m).
    
nlet rec minus (n: Nat) (o: Nat) on n ≝
  match n with
    [ Z ⇒ Z
    | S p ⇒
      match o with
        [ Z ⇒ S p
        | S q ⇒ minus p q
        ]
    ].
    
notation "hvbox(n break - m)"
  right associative with precedence 47
  for @{ 'minus $n $m }.
  
interpretation "Nat minus" 'minus n m = (minus n m).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Multiplication, modulus and division.                                      *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
nlet rec multiplication (n: Nat) (o: Nat) on n ≝
  match n with
    [ Z ⇒ Z
    | S p ⇒ o + (multiplication p o)
    ].
    
notation "hvbox(n break * m)"
  right associative with precedence 47
  for @{ 'multiplication $n $m }.
  
interpretation "Nat multiplication" 'times n m = (multiplication n m).

nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
  match less_than_or_equal_b n p with
    [ true ⇒ Z
    | false ⇒
      match m with
        [ Z ⇒ Z
        | (S q) ⇒ S (division_aux q (n - (S p)) p)
        ]
    ].
    
ndefinition division ≝
  λm, n: Nat.
    match n with
      [ Z ⇒ S m
      | S o ⇒ division_aux m m o
      ].
      
notation "hvbox(n break ÷ m)"
  right associative with precedence 47
  for @{ 'division $n $m }.
  
interpretation "Nat division" 'division n m = (division n m).
      
nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
  match less_than_or_equal_b n p with
    [ true ⇒ n
    | false ⇒
      match m with
        [ Z ⇒ n
        | S o ⇒ modulus_aux o (n - (S p)) p
        ]
    ].
    
ndefinition modulus ≝
  λm, n: Nat.
    match n with
      [ Z ⇒ m
      | S o ⇒ modulus_aux m m o
      ].
    
notation "hvbox(n break 'mod' m)"
  right associative with precedence 47
  for @{ 'modulus $n $m }.
  
interpretation "Nat modulus" 'modulus m n = (modulus m n).

ndefinition divide_with_remainder ≝
  λm, n: Nat.
    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Exponentials, and square roots.                                            *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec exponential (m: Nat) (n: Nat) on n ≝
  match n with
    [ Z ⇒ S (Z)
    | S o ⇒ m * exponential m o
    ].
    
notation "hvbox(n ^ m)"
  left associative with precedence 52
  for @{ 'exponential $n $m }.
  
interpretation "Nat exponential" 'exponential n m = (exponential n m).

nlet rec eq_n (m: Nat) (n: Nat) on m: Bool ≝
  match m with
    [ Z ⇒
      match n with
        [ Z ⇒ true
        | _ ⇒ false
        ]
    | S o ⇒
      match n with
        [ S p ⇒ eq_n o p
        | _ ⇒ false
        ]
    ].

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Greatest common divisor and least common multiple.                         *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Axioms.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

(*naxiom plus_minus_inverse_left:
  ∀m, n: Nat.
    (m + n) - n = m.
*)
  
ntheorem less_than_or_equal_monotone:
  ∀m, n: Nat.
    m ≤ n → (S m) ≤ (S n).
 #m n H; nelim H; /2/.
nqed.

nlemma trans_le: ∀n,m,l. n ≤ m → m ≤ l → n ≤ l.
 #n m l H H1; nelim H1; /2/.
nqed.

ntheorem less_than_or_equal_injective:
  ∀m, n: Nat.
    (S m) ≤ (S n) → m ≤ n.
 #m n H;
 nchange with (match S m with [ Z ⇒ Z | S x ⇒ x] ≤ match S n with [ Z ⇒ Z | S x ⇒ x]);
 napply (match H return λx.λ_. m ≤ match x with [Z ⇒ Z | S x ⇒ x] with [ ltoe_refl ⇒ ? | ltoe_step y H ⇒ ? ]);
 nnormalize; /3/.
nqed.
    
ntheorem succ_less_than_injective:
  ∀m, n: Nat.
    less_than_p (S m) (S n) → m < n.
 /2/.
nqed.

nlemma not_less_than_S_Z:
 ∀m,n: Nat. S m ≤ n → ¬ (n = Z).
 #m n H; nelim H [ @; #K; ndestruct | #y H1 H2; @; #K; ndestruct ]
nqed. 

ntheorem nothing_less_than_Z:
  ∀m: Nat.
    ¬(m < Z).
 #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/;
nqed. 

    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lemmas.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
nlemma less_than_or_equal_zero:
  ∀n: Nat.
    Z ≤ n.
  #n.
  nelim n.
  //.
  #N.
  napply ltoe_step.
nqed.

(*
nlemma less_than_or_equal_zero_equal_zero:
  ∀m: Nat.
    m ≤ Z → m = Z.
  #m.
  nelim m.
  //.
  #N H H2.
  nnormalize.
*)

nlemma less_than_or_equal_reflexive:
  ∀n: Nat.
    n ≤ n.
  #n.
  nelim n.
  nnormalize.
  @.
  #N H.
  nnormalize.
  //.
nqed.

(*
nlemma less_than_or_equal_succ:
  ∀m, n: Nat.
    S m ≤ n → m ≤ n.
  #m n.
  nelim m.
  #H.
  napplyS less_than_or_equal_zero.
  #N H H2.
  nrewrite > H.
  nnormalize.

nlemma less_than_or_equal_transitive:
  ∀m, n, o: Nat.
    m ≤ n ∧ n ≤ o → m ≤ o.
  #m n o.
  nelim m.
  #H.
  napply less_than_or_equal_zero.
  #N H H2.
  nnormalize.
*)

nlemma plus_zero:
  ∀n: Nat.
    n + Z = n.
  #n.
  nelim n.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

nlemma plus_associative:
  ∀m, n, o: Nat.
    (m + n) + o = m + (n + o).
  #m n o.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

nlemma succ_plus:
  ∀m, n: Nat.
    S(m + n) = m + S(n).
  #m n.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

nlemma succ_plus_succ_zero:
  ∀n: Nat.
    S n = plus n (S Z).
  #n.
  nelim n.
  //.
  #N H.
  nnormalize.
  nrewrite < H.
  @.
nqed.

nlemma plus_symmetrical:
  ∀m, n: Nat.
    m + n = n + m.
  #m n.
  nelim m.
  nnormalize.
  nelim n.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite < H.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  napply succ_plus.
nqed.

nlemma multiplication_zero_right_neutral:
  ∀m: Nat.
    m * Z = Z.
  #m.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

nlemma multiplication_succ:
  ∀m, n: Nat.
    m * S(n) = m + (m * n).
  #m n.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite < (plus_associative n N ?).
  nrewrite > (plus_symmetrical n N).
  nrewrite > (plus_associative N n ?).
  @.
nqed.

nlemma multiplication_symmetrical:
  ∀m, n: Nat.
    m * n = n * m.
  #m n.
  nelim m.
  nnormalize.
  nelim n.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite < H.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite > (multiplication_succ ? ?).
  @.
nqed.

nlemma multiplication_succ_zero_left_neutral:
  ∀m: Nat.
    (S Z) * m = m.
  #m.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > (succ_plus ? ?).
  nrewrite < (succ_plus_succ_zero ?).
  @.
nqed.

nlemma multiplication_succ_zero_right_neutral:
  ∀m: Nat.
    m * (S Z) = m.
  #m.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

nlemma multiplication_distributes_right_plus:
  ∀m, n, o: Nat.
    (m + n) * o = m * o + n * o.
  #m n o.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite < (plus_associative ? ? ?).
  @.
nqed.

nlemma multiplication_distributes_left_plus:
  ∀m, n, o: Nat.
    o * (m + n) = o * m + o * n.
  #m n o.
  nelim o.
  //.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite < (plus_associative ? n (N * n)).
  nrewrite > (plus_symmetrical (m + N * m) n).
  nrewrite < (plus_associative n m (N * m)).
  nrewrite < (plus_symmetrical n m).
  nrewrite > (plus_associative (n + m) (N * m) (N * n)).
  @.
nqed.

nlemma mutliplication_associative:
  ∀m, n, o: Nat.
    m * (n * o) = (m * n) * o.
  #m n o.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite > (multiplication_distributes_right_plus ? ? ?).
  @.
nqed.

nlemma minus_minus:
  ∀n: Nat.
    n - n = Z.
  #n.
  nelim n.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.


nlemma succ_injective:
  ∀m, n: Nat.
    S m = S n → m = n.
  #m n H;
  napply (match H return λy.λ_.m = match y with [Z ⇒ Z | S z ⇒ z] with
           [refl ⇒ ? ]);
  @;
nqed.

ntheorem eq_f: ∀A,B:Type[0].∀f:A→B.∀a,a'. a=a' → f a = f a'.
 //;
nqed.

ntheorem plus_minus_inverse_right:
  ∀m, n: Nat.
   n ≤ m → (m - n) + n = m.
 #m; nelim m
  [ #n; nelim n; //; #H1 H2 H3; ncases (nothing_less_than_Z H1);
    #K; ncases (K H3)
  | #y H1 x H2; nnormalize; ngeneralize in match H2; ncases x; nnormalize; /2/;
    #w; nrewrite < succ_plus; /4/. ##]
nqed.

(*

nlemma plus_minus_associate:
  ∀m, n, o: Nat.
    (m + n) - o = m + (n - o).
  #m n o.
  nelim m.
  nnormalize.
  @.
  #N H.
  

nlemma plus_minus_inverses:
  ∀m, n: Nat.
    (m + n) - n = m.
  #m n.
  nelim m.
  nnormalize.
  napply minus_minus.
  #N H.
*)

ntheorem less_than_or_equal_b_correct: ∀m,n. less_than_or_equal_b m n = true → m ≤ n.
 #m; nelim m; //; #y H1 z; ncases z; nnormalize
  [ #H; ndestruct | /3/ ]
nqed.

ntheorem less_than_or_equal_b_complete: ∀m,n. less_than_or_equal_b m n = false → ¬(m ≤ n).
 #m; nelim m; nnormalize
  [ #n H; ndestruct | #y H1 z; ncases z; nnormalize
    [ #H; /2/ | /3/ ]
nqed.

ndefinition less_than_or_equal_b_elim:
 ∀m,n. ∀P: Bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) →
  P (less_than_or_equal_b m n).
 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n);
 nlapply (less_than_or_equal_b_complete m n);
 ncases (less_than_or_equal_b m n); /3/.
nqed.

ndefinition greater_than_or_equal_b_elim:
 ∀m,n. ∀P: Bool → Type[0]. (m ≥ n → P true) → (¬(m ≥ n) → P false) →
  P (greater_than_or_equal_b m n).
 #m n; napply less_than_or_equal_b_elim;
nqed.

ntheorem less_than_b_correct: ∀m,n. less_than_b m n = true → m < n.
 #m; nelim m
  [ #n; ncases n [ #H; nnormalize in H; ndestruct | #z H; /2/ ]
##| #y H z; ncases z [ nnormalize; #K; ndestruct | #o K;
    napply less_than_or_equal_monotone; napply H; napply K ]
nqed.

ntheorem less_than_b_complete: ∀m,n. less_than_b m n = false → ¬(m < n).
 #m; nelim m
  [ #n; ncases n; //; #y H1; nnormalize in H1; ndestruct
  | #y H z; ncases z; //; #o H2; nlapply (H … H2); /3/.
nqed.

ndefinition less_than_b_elim:
 ∀m,n. ∀P: Bool → Type[0]. (m < n → P true) → (¬(m < n) → P false) →
  P (less_than_b m n).
 #m n; nlapply (less_than_b_correct m n); nlapply (less_than_b_complete m n);
 ncases (less_than_b m n); /3/.
nqed.

ndefinition greater_than_b_elim:
 ∀m,n. ∀P: Bool → Type[0]. (m > n → P true) → (¬(m > n) → P false) →
  P (greater_than_b m n).
 #m n; napply less_than_b_elim.
nqed.

nlemma less_than_or_equal_plus:
  ∀n,m: Nat.
    n ≤ n + m.
  #n m.
  nelim n.
  //.
  #N H.
  napply (less_than_or_equal_monotone).
  /2/.
nqed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Numbers.                                                                   *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ndefinition one ≝ S Z.
ndefinition two ≝ (S(S(Z))).
ndefinition three ≝ two + one.
ndefinition four ≝ two + two.
ndefinition five ≝ three + two.
ndefinition six ≝ three + three.
ndefinition seven ≝ three + four.
ndefinition eight ≝ four + four.
ndefinition nine ≝ five + four.
ndefinition ten ≝ five + five.
ndefinition eleven ≝ six + five.
ndefinition twelve ≝ six + six.
ndefinition thirteen ≝ seven + six.
ndefinition fourteen ≝ seven + seven.
ndefinition fifteen ≝ eight + seven.
ndefinition sixteen ≝ eight + eight.
ndefinition seventeen ≝ nine + eight.
ndefinition eighteen ≝ nine + nine.
ndefinition nineteen ≝ ten + nine.
ndefinition twenty_four ≝ sixteen + eight.
ndefinition thirty_two ≝ sixteen + sixteen.
ndefinition one_hundred ≝ ten * ten.
ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
ndefinition two_hundred ≝ one_hundred + one_hundred.
ndefinition two_hundred_and_two ≝ two_hundred + two.
ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
ndefinition two_hundred_and_fifty_six ≝
  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.