proposition: Theorem iff_reflect : forall P b, (P <-> b = true) -> reflect P b.
proof: Proof. intros P b H. destruct b eqn:Eb. - apply ReflectT. rewrite H. reflexivity. - apply ReflectF. rewrite H. intros H'. discriminate. Qed.
imports: Coq(Lia)