proposition: Theorem iff_reflect : forall P b, (P <-> b = true) -> reflect P b.
proof: Proof. Admitted. Lemma eqbP : forall n m, reflect (n = m) (n =? m). Proof. intros n m. apply iff_reflect. rewrite eqb_eq. reflexivity. Qed.
imports: Coq(Lia)