proposition: Theorem iff_sym : forall P Q : Prop, (P <-> Q) -> (Q <-> P).
proof: Proof. Admitted. Lemma not_true_iff_false : forall b, b <> true <-> b = false. Proof. Admitted. Lemma apply_iff_example1: forall P Q R : Prop, (P <-> Q) -> (Q -> R) -> (P -> R). intros P Q R Hiff H HP. apply H. apply Hiff. apply HP. Qed.