Library MetaCoq.Template.utils.MCArith

From Coq Require Import Arith ZArith Lia.

Inductive BoolSpecSet (P Q : Prop) : bool Set :=
    BoolSpecT : P BoolSpecSet P Q true | BoolSpecF : Q BoolSpecSet P Q false.

Lemma leb_spec_Set : x y : nat, BoolSpecSet (x y) (y < x) (x <=? y).
Proof.
  intros.
  destruct (Nat.leb_spec0 x y).
  now constructor.
  constructor. now lia.
Qed.

Lemma nat_rev_ind (max : nat) :
   (P : nat Prop),
    ( n, n max P n)
    ( n, n < max P (S n) P n)
     n, P n.
Proof.
  intros P hmax hS.
  assert (h : n, P (max - n)).
  { intros n. induction n.
    - apply hmax. lia.
    - destruct (Nat.leb_spec0 max n).
      + replace (max - S n) with 0 by lia.
        replace (max - n) with 0 in IHn by lia.
        assumption.
      + replace (max - n) with (S (max - S n)) in IHn by lia.
        apply hS.
        × lia.
        × assumption.
  }
  intro n.
  destruct (Nat.leb_spec0 max n).
  - apply hmax. lia.
  - replace n with (max - (max - n)) by lia. apply h.
Qed.

Lemma strong_nat_ind :
   (P : nat Prop),
    ( n, ( m, m < n P m) P n)
     n, P n.
Proof.
  intros P h n.
  assert ( m, m < n P m).
  { induction n ; intros m hh.
    - lia.
    - destruct (Nat.eqb_spec n m).
      + subst. eapply h. assumption.
      + eapply IHn. lia.
  }
  eapply h. assumption.
Qed.

Lemma Z_of_pos_alt p : Z.of_nat (Pos.to_nat p) = Z.pos p.
Proof.
  induction p using Pos.peano_ind.
  rewrite Pos2Nat.inj_1. reflexivity.
  rewrite Pos2Nat.inj_succ. cbn. f_equal. lia.
Qed.