proposition: Lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R).
proof: Proof. intro f. intro g. destruct f as [pq qp]. destruct g as [gr rg]. split. intro p. apply gr. apply pq. exact p. intro r. apply qp. apply rg. exact r. Qed.
imports: Unicode.Utf8 Classical