proposition: Lemma iff_intro_swap : forall (P Q : Prop), (Q -> P) -> (P -> Q) -> (P <-> Q).
proof: Proof. Proof using. intuition. Qed.
imports: Coq.Lists.List Coq.Logic.ProofIrrelevance Coq.Program.Equality Coq.Arith.Compare_dec Coq.micromega.Lia