proposition: Theorem reflect_iff : forall P b, reflect P b -> (P <-> b = true).
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)