HyPre.util.Misc

(* CLN B *)
From Coq Require Import Lists.List.
Import ListNotations.

Lemma iter_S {X : Type} n (x : X) f
: Nat.iter (S n) f x = f (Nat.iter n f x).
Proof.
  reflexivity.
Qed.

Lemma app_nil_eq {A : Type} (l1 l2 : list A)
  : [] = l1 ++ l2 -> l1 = [] /\ l2 = [].
Proof.
  intros.
  destruct l1,l2;cbn in *;try congruence.
  firstorder.
Qed.

Definition opt_default {X : Type} (default : X) (x : option X) : X
  := match x with
     | Some x => x
     | None => default
     end.

Definition opt_bool {X : Type} (x : option X) : bool
  := match x with Some _ => true | None => false end.

Lemma and_split1 (P Q : Prop)
  : P -> (P -> Q) -> P /\ Q.
Proof.
  clear.
  firstorder.
Qed.