Require Export PeanoNat.

#[global]
Hint Resolve Nat.le_trans: arith. #[global]
Hint Immediate Nat.le_antisymm: arith. #[global]
Hint Resolve Nat.le_0_l Nat.nle_succ_0: arith. #[global]
Hint Resolve Peano.le_n_S Nat.le_succ_diag_r Nat.nle_succ_diag_l : arith. #[local]
Definition le_n_0_eq_stt := fun n Hle => eq_sym (proj1 (Nat.le_0_r n) Hle).
Opaque le_n_0_eq_stt.
#[global]
Hint Immediate le_n_0_eq_stt Nat.lt_le_incl Peano.le_S_n : arith. #[global]
Hint Resolve Nat.le_pred_l: arith. #[global]
Hint Resolve Nat.lt_irrefl: arith. #[local]
Definition lt_le_S_stt := fun n m => (proj2 (Nat.le_succ_l n m)).
Opaque lt_le_S_stt.
#[global]
Hint Immediate lt_le_S_stt: arith. #[local]
Definition lt_n_Sm_le_stt := fun n m => (proj1 (Nat.lt_succ_r n m)).
Opaque lt_n_Sm_le_stt.
#[global]
Hint Immediate lt_n_Sm_le_stt: arith. #[local]
Definition le_lt_n_Sm_stt := fun n m => (proj2 (Nat.lt_succ_r n m)).
Opaque le_lt_n_Sm_stt.
#[global]
Hint Immediate le_lt_n_Sm_stt: arith. #[local]
Definition le_not_lt_stt := fun n m => (proj1 (Nat.le_ngt n m)).
Opaque le_not_lt_stt.
#[global]
Hint Immediate le_not_lt_stt: arith. #[local]
Definition lt_not_le_stt := fun n m => (proj1 (Nat.lt_nge n m)).
Opaque lt_not_le_stt.
#[global]
Hint Immediate lt_not_le_stt: arith. #[global]
Hint Resolve Nat.lt_0_succ Nat.nlt_0_r: arith. #[local]
Definition neq_0_lt_stt := fun n Hn => proj1 (Nat.neq_0_lt_0 n) (Nat.neq_sym 0 n Hn).
Opaque neq_0_lt_stt.
#[local]
Definition lt_0_neq_stt := fun n Hlt => Nat.neq_sym n 0 (proj2 (Nat.neq_0_lt_0 n) Hlt).
Opaque lt_0_neq_stt.
#[global]
Hint Immediate neq_0_lt_stt lt_0_neq_stt: arith. #[global]
Hint Resolve Nat.lt_succ_diag_r Nat.lt_lt_succ_r: arith. #[local]
Definition lt_n_S_stt := fun n m => (proj1 (Nat.succ_lt_mono n m)).
Opaque lt_n_S_stt.
#[global]
Hint Resolve lt_n_S_stt: arith. #[local]
Definition lt_S_n_stt := fun n m => (proj2 (Nat.succ_lt_mono n m)).
Opaque lt_S_n_stt.
#[global]
Hint Immediate lt_S_n_stt: arith. #[local]
Definition lt_pred_stt := fun n m => proj1 (Nat.lt_succ_lt_pred n m).
Opaque lt_pred_stt.
#[global]
Hint Immediate lt_pred_stt: arith. #[local]
Definition lt_pred_n_n_stt := fun n Hlt => Nat.lt_pred_l n (proj2 (Nat.neq_0_lt_0 n) Hlt).
Opaque lt_pred_n_n_stt.
#[global]
Hint Resolve lt_pred_n_n_stt: arith. #[global]
Hint Resolve Nat.lt_trans Nat.lt_le_trans Nat.le_lt_trans: arith. #[global]
Hint Immediate Nat.lt_le_incl: arith. #[local]
Definition gt_Sn_O_stt : forall n, S n > 0 := Nat.lt_0_succ.
Opaque gt_Sn_O_stt.
#[global]
Hint Resolve gt_Sn_O_stt: arith. #[local]
Definition gt_Sn_n_stt : forall n, S n > n := Nat.lt_succ_diag_r.
Opaque gt_Sn_n_stt.
#[global]
Hint Resolve gt_Sn_n_stt: arith. #[local]
Definition gt_n_S_stt : forall n m, n > m -> S n > S m := fun n m Hgt => proj1 (Nat.succ_lt_mono m n) Hgt.
Opaque gt_n_S_stt.
#[global]
Hint Resolve gt_n_S_stt: arith. #[local]
Definition gt_S_n_stt : forall n m, S m > S n -> m > n := fun n m Hgt => proj2 (Nat.succ_lt_mono n m) Hgt.
Opaque gt_S_n_stt.
#[global]
Hint Immediate gt_S_n_stt: arith. #[local]
Definition gt_pred_stt : forall n m, m > S n -> pred m > n := fun n m Hgt => proj1 (Nat.lt_succ_lt_pred n m) Hgt.
Opaque gt_pred_stt.
#[global]
Hint Immediate gt_pred_stt: arith. #[local]
Definition gt_irrefl_stt : forall n, ~ n > n := Nat.lt_irrefl.
Opaque gt_irrefl_stt.
#[global]
Hint Resolve gt_irrefl_stt: arith. #[local]
Definition gt_asym_stt : forall n m, n > m -> ~ m > n := fun n m => Nat.lt_asymm m n.
Opaque gt_asym_stt.
#[global]
Hint Resolve gt_asym_stt: arith. #[local]
Definition le_not_gt_stt : forall n m, n <= m -> ~ n > m := fun n m => proj1 (Nat.le_ngt n m).
Opaque le_not_gt_stt.
#[global]
Hint Resolve le_not_gt_stt: arith. #[local]
Definition gt_not_le_stt: forall n m, n > m -> ~ n <= m := fun n m => proj1 (Nat.lt_nge m n).
Opaque gt_not_le_stt.
#[global]
Hint Resolve gt_not_le_stt: arith. #[local]
Definition le_S_gt_stt: forall n m, S n <= m -> m > n := fun n m => proj1 (Nat.le_succ_l n m).
Opaque le_S_gt_stt.
#[global]
Hint Immediate le_S_gt_stt:arith. #[local]
Definition gt_S_le_stt : forall n m, S m > n -> n <= m := fun n m => proj2 (Nat.succ_le_mono n m).
Opaque gt_S_le_stt.
#[global]
Hint Immediate gt_S_le_stt:arith. #[local]
Definition gt_le_S_stt : forall n m, m > n -> S n <= m := fun n m => proj2 (Nat.le_succ_l n m).
Opaque gt_le_S_stt.
#[global]
Hint Resolve gt_le_S_stt:arith. #[local]
Definition le_gt_S_stt : forall n m, n <= m -> S m > n := fun n m => proj1 (Nat.succ_le_mono n m).
Opaque le_gt_S_stt.
#[global]
Hint Resolve le_gt_S_stt:arith. #[local]
Definition gt_trans_S_stt : forall n m p, S n > m -> m > p -> n > p
                          := fun n m p Hgt1 Hgt2 => Nat.lt_le_trans p m n Hgt2 (proj2 (Nat.succ_le_mono _ _) Hgt1).
Opaque gt_trans_S_stt.
#[global]
Hint Resolve gt_trans_S_stt:arith. #[local]
Definition le_gt_trans_stt : forall n m p, m <= n -> m > p -> n > p
                           := fun n m p Hle Hgt => Nat.lt_le_trans p m n Hgt Hle.
Opaque le_gt_trans_stt.
#[global]
Hint Resolve le_gt_trans_stt:arith. #[local]
Definition gt_le_trans_stt : forall n m p, n > m -> p <= m -> n > p
                           := fun n m p Hgt Hle => Nat.le_lt_trans p m n Hle Hgt.
Opaque gt_le_trans_stt.
#[global]
Hint Resolve gt_le_trans_stt:arith. #[local]
Definition plus_gt_compat_l_stt : forall n m p, n > m -> p + n > p + m
                                := fun n m p Hgt => proj1 (Nat.add_lt_mono_l m n p) Hgt.
Opaque plus_gt_compat_l_stt.
#[global]
Hint Resolve plus_gt_compat_l_stt:arith.
#[global]
Hint Immediate Nat.add_comm : arith. #[global]
Hint Resolve Nat.add_assoc : arith. #[local]
Definition plus_assoc_reverse_stt := fun n m p => eq_sym (Nat.add_assoc n m p).
Opaque plus_assoc_reverse_stt.
#[global]
Hint Resolve plus_assoc_reverse_stt : arith. #[global]
Hint Resolve -> Nat.add_le_mono_l : arith. #[global]
Hint Resolve -> Nat.add_le_mono_r : arith. #[local]
Definition le_plus_r_stt := (fun n m => Nat.le_add_l m n).
#[local]
Definition le_plus_trans_stt := (fun n m p Hle => Nat.le_trans n _ _ Hle (Nat.le_add_r m p)).
Opaque le_plus_r_stt le_plus_trans_stt.
#[global]
Hint Resolve Nat.le_add_r le_plus_r_stt le_plus_trans_stt : arith. #[local]
Definition lt_plus_trans_stt := (fun n m p Hlt => Nat.lt_le_trans n _ _ Hlt (Nat.le_add_r m p)).
Opaque lt_plus_trans_stt.
#[global]
Hint Immediate lt_plus_trans_stt : arith. #[global]
Hint Resolve -> Nat.add_lt_mono_l : arith. #[global]
Hint Resolve -> Nat.add_lt_mono_r : arith.
#[local]
Definition minus_n_O_stt := fun n => eq_sym (Nat.sub_0_r n).
Opaque minus_n_O_stt.
#[global]
Hint Resolve minus_n_O_stt: arith. #[local]
Definition minus_Sn_m_stt := fun n m Hle => eq_sym (Nat.sub_succ_l m n Hle).
Opaque minus_Sn_m_stt.
#[global]
Hint Resolve minus_Sn_m_stt: arith. #[local]
Definition minus_diag_reverse_stt := fun n => eq_sym (Nat.sub_diag n).
Opaque minus_diag_reverse_stt.
#[global]
Hint Resolve minus_diag_reverse_stt: arith. #[local]
Definition minus_plus_simpl_l_reverse_stt n m p : n - m = p + n - (p + m).
#[global]
Hint Resolve minus_plus_simpl_l_reverse_stt: arith. #[local]
Definition plus_minus_stt := fun n m p Heq => eq_sym (Nat.add_sub_eq_l n m p (eq_sym Heq)).
Opaque plus_minus_stt.
#[global]
Hint Immediate plus_minus_stt: arith. #[local]
Definition minus_plus_stt := (fun n m => eq_ind _ (fun x => x - n = m) (Nat.add_sub m n) _ (Nat.add_comm _ _)).
Opaque minus_plus_stt.
#[global]
Hint Resolve minus_plus_stt: arith. #[local]
Definition le_plus_minus_stt := fun n m Hle => eq_sym (eq_trans (Nat.add_comm _ _) (Nat.sub_add n m Hle)).
Opaque le_plus_minus_stt.
#[global]
Hint Resolve le_plus_minus_stt: arith. #[local]
Definition le_plus_minus_r_stt := fun n m Hle => eq_trans (Nat.add_comm _ _) (Nat.sub_add n m Hle).
Opaque le_plus_minus_r_stt.
#[global]
Hint Resolve le_plus_minus_r_stt: arith. #[global]
Hint Resolve Nat.sub_lt: arith. #[local]
Definition lt_O_minus_lt_stt : forall n m, 0 < n - m -> m < n
                            := fun n m => proj2 (Nat.lt_add_lt_sub_r 0 n m).
Opaque lt_O_minus_lt_stt.
#[global]
Hint Immediate lt_O_minus_lt_stt: arith.
#[global]
Hint Resolve Nat.mul_1_l Nat.mul_1_r: arith. #[global]
Hint Resolve Nat.mul_comm: arith. #[global]
Hint Resolve Nat.mul_add_distr_r: arith. #[global]
Hint Resolve Nat.mul_sub_distr_r: arith. #[global]
Hint Resolve Nat.mul_sub_distr_l: arith. #[local]
Definition mult_assoc_reverse_stt := fun n m p => eq_sym (Nat.mul_assoc n m p).
Opaque mult_assoc_reverse_stt.
#[global]
Hint Resolve mult_assoc_reverse_stt Nat.mul_assoc: arith. #[local]
Definition mult_O_le_stt n m : m = 0 \/ n <= m * n.
#[global]
Hint Resolve mult_O_le_stt: arith. #[global]
Hint Resolve Nat.mul_le_mono_l: arith. #[local]
Definition mult_S_lt_compat_l_stt := (fun n m p Hlt => proj1 (Nat.mul_lt_mono_pos_l (S n) m p (Nat.lt_0_succ n)) Hlt).
Opaque mult_S_lt_compat_l_stt.
#[global]
Hint Resolve mult_S_lt_compat_l_stt: arith.
#[global]
Hint Resolve Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r: arith.
#[global]
Hint Resolve Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r: arith.

#[global]
Hint Constructors Nat.Even_alt: arith.
#[global]
Hint Constructors Nat.Odd_alt: arith.

#[local]
Definition lt_n_Sm_le := (fun n m => (proj1 (Nat.lt_succ_r n m))).
Register lt_n_Sm_le as num.nat.lt_n_Sm_le.
#[local]
Definition le_lt_n_Sm := (fun n m => (proj2 (Nat.lt_succ_r n m))).
Register le_lt_n_Sm as num.nat.le_lt_n_Sm.
#[local]
Definition lt_S_n := (fun n m => (proj2 (Nat.succ_lt_mono n m))).
Register lt_S_n as num.nat.lt_S_n.
Register Nat.le_lt_trans as num.nat.le_lt_trans.
#[local]
Definition pred_of_minus := (fun n => eq_sym (Nat.sub_1_r n)).
Register pred_of_minus as num.nat.pred_of_minus.