(* File automatically generated by Hacspec *)
From Coq Require Import ZArith.
Require Import List.
Import List.ListNotations.
Open Scope Z_scope.
Open Scope bool_scope.
Require Import Ascii.
Require Import String.
Require Import Coq.Floats.Floats.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.

(* From Core Require Import Core. *)

From Core Require Import Core_Base_Spec.
Export Core_Base_Spec.

From Core Require Import Core_Cmp.
Export Core_Cmp.

From Core Require Import Core_Option.
Export Core_Option.

From Core Require Import Core_Clone.
Export Core_Clone.

Fixpoint positive_cmp__cmp_binary_cont (x : t_Positive) (y : t_Positive) (r : t_Ordering) : t_Ordering :=
  match match_positive (x) with
  | POSITIVE_XH =>
    match match_positive (y) with
    | POSITIVE_XH =>
      r
    | POSITIVE_XO (q)
    | POSITIVE_XI (q) =>
      Ordering_Less
    end
  | POSITIVE_XO (p) =>
    match match_positive (y) with
    | POSITIVE_XH =>
      Ordering_Greater
    | POSITIVE_XO (q) =>
      positive_cmp__cmp_binary_cont (p) (q) (r)
    | POSITIVE_XI (q) =>
      positive_cmp__cmp_binary_cont (p) (q) (Ordering_Less)
    end
  | POSITIVE_XI (p) =>
    match match_positive (y) with
    | POSITIVE_XH =>
      Ordering_Greater
    | POSITIVE_XO (q) =>
      positive_cmp__cmp_binary_cont (p) (q) (Ordering_Greater)
    | POSITIVE_XI (q) =>
      positive_cmp__cmp_binary_cont (p) (q) (r)
    end
  end.

Definition positive_cmp (lhs : t_Positive) (rhs : t_Positive) : t_Ordering :=
  positive_cmp__cmp_binary_cont (lhs) (rhs) (Ordering_Equal).

Definition positive_le (lhs : t_Positive) (rhs : t_Positive) : bool :=
  match Option_Some (positive_cmp (lhs) (rhs)) with
  | Option_Some (Ordering_Less
  | Ordering_Equal) =>
    true
  | _ =>
    false
  end.

Fixpoint positive_pred_double (s : t_Positive) : t_Positive :=
  match match_positive (s) with
  | POSITIVE_XH =>
    xH
  | POSITIVE_XO (p) =>
    xI (positive_pred_double (p))
  | POSITIVE_XI (p) =>
    xI (xO (p))
  end.

Fixpoint positive_succ (s : t_Positive) : t_Positive :=
  match match_positive (s) with
  | POSITIVE_XH =>
    xO (xH)
  | POSITIVE_XO (q) =>
    xI (q)
  | POSITIVE_XI (q) =>
    xO (positive_succ (q))
  end.

Fixpoint positive_add__add (lhs : t_Positive) (rhs : t_Positive) : t_Positive :=
  match match_positive (lhs) with
  | POSITIVE_XH =>
    match match_positive (rhs) with
    | POSITIVE_XH =>
      xO (xH)
    | POSITIVE_XO (q) =>
      xI (q)
    | POSITIVE_XI (q) =>
      xO (positive_succ (q))
    end
  | POSITIVE_XO (p) =>
    match match_positive (rhs) with
    | POSITIVE_XH =>
      xI (p)
    | POSITIVE_XO (q) =>
      xO (positive_add__add (p) (q))
    | POSITIVE_XI (q) =>
      xI (positive_add__add (p) (q))
    end
  | POSITIVE_XI (p) =>
    match match_positive (rhs) with
    | POSITIVE_XH =>
      xO (positive_succ (p))
    | POSITIVE_XO (q) =>
      xI (positive_add__add (p) (q))
    | POSITIVE_XI (q) =>
      xO (positive_add__add_carry (p) (q))
    end
  end

with positive_add__add_carry (lhs : t_Positive) (rhs : t_Positive) : t_Positive :=
  match match_positive (lhs) with
  | POSITIVE_XH =>
    match match_positive (rhs) with
    | POSITIVE_XH =>
      xI (xH)
    | POSITIVE_XO (q) =>
      xO (positive_succ (q))
    | POSITIVE_XI (q) =>
      xI (positive_succ (q))
    end
  | POSITIVE_XO (p) =>
    match match_positive (rhs) with
    | POSITIVE_XH =>
      xO (positive_succ (p))
    | POSITIVE_XO (q) =>
      xI (positive_add__add (p) (q))
    | POSITIVE_XI (q) =>
      xO (positive_add__add_carry (p) (q))
    end
  | POSITIVE_XI (p) =>
    match match_positive (rhs) with
    | POSITIVE_XH =>
      xI (positive_succ (p))
    | POSITIVE_XO (q) =>
      xO (positive_add__add_carry (p) (q))
    | POSITIVE_XI (q) =>
      xI (positive_add__add_carry (p) (q))
    end
  end.

Definition positive_add (lhs : t_Positive) (rhs : t_Positive) : t_Positive :=
  positive_add__add (lhs) (rhs).

Fixpoint positive_mul (lhs : t_Positive) (rhs : t_Positive) : t_Positive :=
  match match_positive (lhs) with
  | POSITIVE_XH =>
    rhs
  | POSITIVE_XO (p) =>
    xO (positive_mul (p) (rhs))
  | POSITIVE_XI (p) =>
    positive_add (Clone_f_clone (rhs)) (xO (positive_mul (p) (rhs)))
  end.
