HyPre.util.NatExtra

From Coq Require Export Morphisms NPeano Lia.

Global Instance Proper_le_sub
: forall m, Proper (le ==> le) (fun n => n - m).
Proof.
  unfold Proper, respectful.
  intros.
  eapply Nat.sub_le_mono_r;eauto.
Qed.

Global Instance Proper_le_min
  : Proper (le ==> le ==> le) Nat.min.
Proof.
  unfold Proper, respectful.
  intros.
  lia.
Qed.

Global Instance max_le_proper
  : Proper (le ==> le ==> le) Nat.max.
Proof.
  unfold Proper,respectful.
  lia.
Qed.

Global Instance add_le_proper
  : Proper (le ==> le ==> le) Nat.add.
Proof.
  unfold Proper,respectful.
  lia.
Qed.

Global Instance S_le_proper
  : Proper (le ==> le) S.
Proof.
  unfold Proper,respectful.
  lia.
Qed.

Definition gtz (n : nat) : bool
  := match n with
     | 0 => false
     | S _ => true
     end.