Lemma reflect_back : forall b P,
    (b = true <-> P) -> (b = false <-> ~P).
Proof.
  intros b P H.
  split; try firstorder.
  - intros nP.
    assert (b = true). { firstorder. }
    congruence.
  - destruct b; try firstorder.
Qed.

Definition Reflects_P_b (b:bool) (P:Prop) := (b = true <-> P).

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => leb n' m'
      end
  end.

Lemma le_reflects_LE : forall n m,
  Reflects_P_b (leb n m) (n <= m).
Proof.